mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.restrict_RankOne_hom_eq : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (K : Type u_3) [inst_1 : DivisionRing K]
  (v : Valuation K Γ₀) [inst_2 : v.RankOne],
  Valuation.RankOne.hom v.restrict = (Valuation.RankOne.hom v).comp MonoidWithZeroHom.ValueGroup₀.embedding
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.coe_ofBijective : ∀ {F : Type u_1} {A : Type u_3} {B : Type u_4} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : FunLike F A B]
  [inst_5 : NonUnitalRingHomClass F A B] [inst_6 : NonUnitalStarRingHomClass F A B] {f : F}
  (hf : Function.Bijective ⇑f), ⇑(StarRingEquiv.ofBijective f hf) = ⇑f
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.State.map : Lean.Meta.Match.Extension.State → Lean.SMap Lean.Name Lean.Meta.MatcherInfo
-- Mathlib.Order.Heyting.Basic
sdiff_le_iff_left : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, b \ a ≤ a ↔ b ≤ a
-- Batteries.Data.List.Lemmas
List.getElem_zero_idxsOf_eq_idxOf_add : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α] (h : 0 < (List.idxsOf x xs s).length),
  (List.idxsOf x xs s)[0] = List.idxOf x xs + s
-- Mathlib.Topology.Hom.ContinuousEval
ContinuousWithinAt.eval : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y] [inst_5 : TopologicalSpace Z]
  {f : Z → F} {g : Z → X} {s : Set Z} {z : Z},
  ContinuousWithinAt f s z → ContinuousWithinAt g s z → ContinuousWithinAt (fun z => (f z) (g z)) s z
-- Mathlib.Analysis.Complex.Basic
Complex.instContinuousStar : ContinuousStar ℂ
-- Mathlib.Topology.Algebra.Module.Complement
/-- **Alias** of the reverse direction of `Submodule.projectionL_apply_eq_zero_iff`. -/
Submodule.projectionL_apply_eq_zero_of_mem_right : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) {x : M}, x ∈ q → (p.projectionL q h) x = 0
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.cuspFunction_mul : ∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  ContinuousAt (UpperHalfPlane.cuspFunction h f) 0 →
    ContinuousAt (UpperHalfPlane.cuspFunction h g) 0 →
      UpperHalfPlane.cuspFunction h (f * g) = UpperHalfPlane.cuspFunction h f * UpperHalfPlane.cuspFunction h g
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
/-- Construct a continuous linear map from a linear map and the existence of a bound on this linear
map. If you have an explicit bound, use `LinearMap.mkContinuous` instead, as a norm estimate will
follow automatically in `LinearMap.mkContinuous_norm_le`.  -/
LinearMap.mkContinuousOfExistsBound : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_3} →
      {F : Type u_4} →
        [inst : Ring 𝕜] →
          [inst_1 : Ring 𝕜₂] →
            [inst_2 : SeminormedAddCommGroup E] →
              [inst_3 : SeminormedAddCommGroup F] →
                [inst_4 : Module 𝕜 E] →
                  [inst_5 : Module 𝕜₂ F] →
                    {σ : 𝕜 →+* 𝕜₂} → (f : E →ₛₗ[σ] F) → (∃ C, ∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → E →SL[σ] F
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : α) →
          ((fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (x : α) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l : Std.DTreeMap.Internal.Impl α β) →
                        (size_1 : ℕ) →
                          (k_1 : α) →
                            (v_1 : β k_1) →
                              (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                                (fallback : α) →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner size k v l
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                    fallback) →
                motive x x_1
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzOnWith_iff_norm_neg_add_le`. -/
LipschitzOnWith.norm_neg_add_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {s : Set E} {f : E → F}
  {C : NNReal}, LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖-f x + f y‖ ≤ ↑C * ‖-x + y‖
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of two monotone functions is monotone.  -/
Monotone.add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [AddLeftMono α]
  [AddRightMono α], Monotone f → Monotone g → Monotone fun x => f x + g x
-- Aesop.Index
Aesop.Index.mk : {α : Type} →
  Lean.Meta.DiscrTree (Aesop.Rule α) → Lean.Meta.DiscrTree (Aesop.Rule α) → Lean.PHashSet (Aesop.Rule α) → Aesop.Index α
-- Lean.Widget.UserWidget
/-- Output of `getWidgets` RPC. -/
Lean.Widget.GetWidgetsResponse : Type
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- The trivial hypergraph with a given vertex set is defined by having no edges on that vertex
set.  -/
Hypergraph.trivialOn : {α : Type u_1} → Set α → Hypergraph α
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- Multiple transitivity of a pretransitive action
is equivalent to one less transitivity of stabilizer of a point
(Wielandt, th. 9.1, 1st part)  -/
SubMulAction.ofStabilizer.isMultiplyPretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [MulAction.IsPretransitive G α] {n : ℕ}
  {a : α},
  MulAction.IsMultiplyPretransitive G α n.succ ↔
    MulAction.IsMultiplyPretransitive (↥(MulAction.stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) n
-- Mathlib.Data.Set.Sigma
Set.exists_sigma_iff : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α i → Prop},
  (∃ x ∈ s.sigma t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p ⟨i, a⟩
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Any matrix can be written as the product of transvections, a diagonal matrix, and
transvections.  -/
Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec : ∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n 𝕜),
  ∃ L L' D,
    M =
      (List.map Matrix.TransvectionStruct.toMatrix L).prod * Matrix.diagonal D *
        (List.map Matrix.TransvectionStruct.toMatrix L').prod
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.epi_left_of_epi : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {G : CategoryTheory.Functor A T} {X : T} [CategoryTheory.Limits.HasPushouts A]
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan G]
  {Y Z : CategoryTheory.CostructuredArrow G X} (f : Y ⟶ Z) [CategoryTheory.Epi f], CategoryTheory.Epi f.left
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ},
  Std.DTreeMap.foldrM f init t = Array.foldrM (fun a b => f a.fst a.snd b) init t.toArray
-- Mathlib.Analysis.Complex.Exponential
Real.le_inv_mul_exp : ∀ (x : ℝ) {c : ℝ}, 0 < c → x ≤ c⁻¹ * Real.exp (c * x)
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.topologicalClosure_coe : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] {s : Subgroup G},
  ↑s.topologicalClosure = closure ↑s
-- Mathlib.Algebra.Module.Presentation.Basic
/-- The sequence `(relations.R →₀ A) → (relations.G →₀ A) → M → 0` is exact.  -/
Module.Relations.Solution.IsPresentation.exact : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M},
  solution.IsPresentation → Function.Exact ⇑relations.map ⇑solution.π
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.isFixedPt_reflectionPerm_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι} [NeZero 2]
  [IsDomain R] [Module.IsTorsionFree R M], Function.IsFixedPt (⇑(P.reflectionPerm i)) j ↔ P.pairing i j = 0
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Composition as an additive monoid homomorphism.  -/
CompactlySupportedContinuousMap.compAddMonoidHom : {β : Type u_3} →
  {γ : Type u_4} →
    {δ : Type u_5} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : AddMonoid δ] →
              [inst_4 : ContinuousAdd δ] →
                CocompactMap β γ → CompactlySupportedContinuousMap γ δ →+ CompactlySupportedContinuousMap β δ
-- Mathlib.Algebra.Category.Ring.Instances
Localization.epi' : ∀ {R : CommRingCat} (M : Submonoid ↑R), CategoryTheory.Epi (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))
-- Mathlib.Data.Semiquot
Semiquot.isPure_univ : ∀ {α : Type u_1} [inst : Inhabited α], Semiquot.univ.IsPure ↔ Subsingleton α
-- Mathlib.Analysis.CStarAlgebra.Spectrum
CStarAlgebra.toReal_spectralRadius_star_mul_self_eq_norm_sq : ∀ {A : Type u_1} [inst : CStarAlgebra A] (a : A), (spectralRadius ℂ (star a * a)).toReal = ‖a‖ ^ 2
-- Mathlib.Probability.Density
/-- **The Law of the Unconscious Statistician**: Given a random variable `X` and a measurable
function `f`, `f ∘ X` is a random variable with expectation `∫ x, pdf X x • f x ∂μ`
where `μ` is a measure on the codomain of `X`.  -/
MeasureTheory.pdf.integral_pdf_smul : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {F : Type u_3} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [MeasureTheory.IsFiniteMeasure ℙ] {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ] {f : E → F},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∫ (x : E), (MeasureTheory.pdf X ℙ μ x).toReal • f x ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.Context.mk.inj : ∀ {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
-- Lean.Elab.MutualDef
Lean.Elab.Term.deprecated.oldSectionVars : Lean.Option Bool
-- Init.GetElem
List.get?Internal_eq_getElem? : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.get?Internal i = l[i]?
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.noSibling_tail : ∀ {α : Type u_1} (le : α → α → Bool) (s : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.tail le s).NoSibling
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Module.End.isRoot_of_hasEigenvalue : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {f : Module.End R M} {μ : R}, f.HasEigenvalue μ → (minpoly R f).IsRoot μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldlM_eq_foldlM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.ExtTreeMap.foldlM f init t = List.foldlM (fun a b => f a b.1 b.2) init t.toList
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF → ∀ {a k : α} {v : β k}, (t.insert k v).get? a = if h : cmp k a = Ordering.eq then some (cast ⋯ v) else t.get? a
-- Mathlib.Tactic.Simps.Basic
/-- Parse a rule for `initialize_simps_projections`. It is `<name>→<name>`, `-<name>`, `+<name>`
or `as_prefix <name>`.  -/
Simps.elabSimpsRule : Lean.Syntax → Lean.Elab.Command.CommandElabM Simps.ProjectionRule
-- Mathlib.Data.List.Zip
List.zipWith_zipWith_left : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} {δ : Type u_3} {ε : Type u_4} (f : δ → γ → ε) (g : α → β → δ) (la : List α)
  (lb : List β) (lc : List γ),
  List.zipWith f (List.zipWith g la lb) lc = List.zipWith3 (fun a b c => f (g a b) c) la lb lc
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {fallback : β} {f : β → β}, (t.modify k f).getD k fallback = (Option.map f t[k]?).getD fallback
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.visitConst : Lean.Name → Lean.Meta.Try.Collector.M Unit
-- Init.Data.Vector.Lemmas
Vector.set_append_left : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i : ℕ} {x : α} (h : i < n),
  (xs ++ ys).set i x ⋯ = xs.set i x h ++ ys
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instHasColimits : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)],
  CategoryTheory.Limits.HasColimits (GeneratedByTopCat X)
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sigmaFiberAddEquiv_of : ∀ {ι₁ ι₂ : Type v} [inst : DecidableEq ι₂] (f : ι₁ → ι₂) {β : ι₁ → Type w} [inst_1 : (i : ι₁) → AddCommMonoid (β i)]
  [inst_2 : DecidableEq ι₁] (i : ι₁) (x : β i),
  (DirectSum.sigmaFiberAddEquiv f) ((DirectSum.of β i) x) =
    (DirectSum.of (fun i => DirectSum { i_1 // f i_1 = i } fun i_1 => β ↑i_1) (f i))
      ((DirectSum.of (fun i_1 => β ↑i_1) ⟨i, ⋯⟩) x)
-- Init.Data.Array.MinMax
Array.isSome_min?_iff : ∀ {α : Type u_1} {xs : Array α} [inst : Min α], xs.min?.isSome = true ↔ xs ≠ #[]
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Integrability in the change of variable formula for differentiable functions: if a
function `f` is injective and differentiable on a measurable set `s`, then a function
`g : E → F` is integrable on `f '' s` if and only if `|(f' x).det| • g ∘ f` is
integrable on `s`.  -/
MeasureTheory.integrableOn_image_iff_integrableOn_abs_det_fderiv_smul : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {s : Set E} {f : E → E} {f' : E → E →L[ℝ] E}
  [inst_5 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        ∀ (g : E → F),
          MeasureTheory.IntegrableOn g (f '' s) μ ↔ MeasureTheory.IntegrableOn (fun x => |(f' x).det| • g (f x)) s μ
-- Mathlib.Algebra.Group.Defs
inv_mul_cancel_right : ∀ {G : Type u_1} [inst : Group G] (a b : G), a * b⁻¹ * b = a
-- Mathlib.Analysis.Asymptotics.Lemmas
/-- Transfer `IsLittleO` over an `OpenPartialHomeomorph`.  -/
OpenPartialHomeomorph.isLittleO_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {E : Type u_3}
  [inst_2 : Norm E] {F : Type u_4} [inst_3 : Norm F] (e : OpenPartialHomeomorph α β) {b : β},
  b ∈ e.target → ∀ {f : β → E} {g : β → F}, f =o[nhds b] g ↔ (f ∘ ↑e) =o[nhds (↑e.symm b)] (g ∘ ↑e)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C}
  {A : C} {toPrecylinder : HomotopicalAlgebra.Precylinder A}
  {weakEquivalence_π :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrecylinder.π)
      HomotopicalAlgebra.Cylinder.weakEquivalence_π._autoParam}
  {toPrecylinder_1 : HomotopicalAlgebra.Precylinder A}
  {weakEquivalence_π_1 :
    autoParam (HomotopicalAlgebra.WeakEquivalence toPrecylinder_1.π)
      HomotopicalAlgebra.Cylinder.weakEquivalence_π._autoParam},
  { toPrecylinder := toPrecylinder, weakEquivalence_π := weakEquivalence_π } =
      { toPrecylinder := toPrecylinder_1, weakEquivalence_π := weakEquivalence_π_1 } →
    toPrecylinder = toPrecylinder_1
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.ext : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L₁' L₂' : LieRinehartSubalgebra A L), (∀ (x : L), x ∈ L₁' ↔ x ∈ L₂') → L₁' = L₂'
-- Mathlib.RepresentationTheory.Invariants
Representation.averageMap.eq_1 : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) [inst_4 : Fintype G] [inst_5 : Invertible ↑(Fintype.card G)],
  ρ.averageMap = ρ.asAlgebraHom (GroupAlgebra.average k G)
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.incl_obj : ∀ (self : CategoryTheory.ObjectProperty.FullSubcategory Finite), FintypeCat.incl.obj self = self.obj
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_max?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km : α} (hc : k ∈ t),
  t.max?.get ⋯ = km → (cmp k km).isLE = true
-- Lean.DocString.Extension
Lean.getVersoModuleDocs : Lean.Environment → Lean.VersoModuleDocs
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.of_mul_t : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (b : ↥B),
  HNNExtension.of ↑b * HNNExtension.t = HNNExtension.t * HNNExtension.of ↑(φ.symm b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₂` and `f₃`.  -/
CategoryTheory.Limits.ChosenPullback₃.p₂₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {f₃ : X₃ ⟶ S} →
            {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
              {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃} →
                {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} →
                  (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) → h.pullback ⟶ h₂₃.pullback
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.mk.injEq : ∀ (carrier : Type u) [str : Mul carrier] (carrier_1 : Type u) (str_1 : Mul carrier_1),
  ({ carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 }) = (carrier = carrier_1 ∧ str ≍ str_1)
-- Batteries.Data.List.Basic
List.zipWithLeftTR.go.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : Array γ) (a_1 : α) (as : List α) (b : β)
  (bs : List β),
  List.zipWithLeftTR.go f (a_1 :: as) (b :: bs) a = List.zipWithLeftTR.go f as bs (a.push (f a_1 (some b)))
-- Mathlib.Data.Seq.Computation
Computation.results_of_terminates' : ∀ {α : Type u} (s : Computation α) [T : s.Terminates] {a : α}, a ∈ s → s.Results a s.length
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
/-- If an object property `P` is closed under kernels, then `P.ι` creates kernels.
In particular, this implies `P.ι` preserves kernels.  -/
CategoryTheory.ObjectProperty.createsKernels : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P : CategoryTheory.ObjectProperty C) →
        [P.IsClosedUnderKernels] →
          {X Y : P.FullSubcategory} →
            (f : X ⟶ Y) →
              [CategoryTheory.Limits.HasKernel f.hom] →
                CategoryTheory.CreatesLimit (CategoryTheory.Limits.parallelPair f 0) P.ι
-- Std.Http.Data.Status
Std.Http.Status.earlyHints.sizeOf_spec : sizeOf Std.Http.Status.earlyHints = 1
-- Mathlib.Data.Int.Bitwise
Int.ldiff.eq_4 : ∀ (m n : ℕ), (Int.negSucc m).ldiff (Int.negSucc n) = ↑(n.ldiff m)
-- Mathlib.Algebra.AffineMonoid.Basic
IsAffineMonoid.toIsMulTorsionFree : ∀ {M : Type u_1} {inst : CommMonoid M} [self : IsAffineMonoid M], IsMulTorsionFree M
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.distribMulAction : {R : Type u_1} →
  {R₂ : Type u_2} →
    {S₃ : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : Semiring R₂] →
          [inst_2 : Monoid S₃] →
            {M : Type u_6} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : Module R M] →
                    {M₂ : Type u_7} →
                      [inst_6 : TopologicalSpace M₂] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R₂ M₂] →
                            {σ₁₂ : R →+* R₂} →
                              [inst_9 : DistribMulAction S₃ M₂] →
                                [ContinuousConstSMul S₃ M₂] →
                                  [SMulCommClass R₂ S₃ M₂] →
                                    [inst_12 : ContinuousAdd M₂] → DistribMulAction S₃ (M →SL[σ₁₂] M₂)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_ne_one : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α], |a|ₘ ≠ 1 ↔ a ≠ 1
-- Mathlib.Data.List.Nodup
List.Nodup.head_eq_getLast_iff : ∀ {α : Type u} {l : List α} (hne : l ≠ []), l.Nodup → (l.head hne = l.getLast hne ↔ ∃ x, l = [x])
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
/-- The inverse image under a monoidal functor of a monoidal morphism property which respects
isomorphisms is monoidal.  -/
CategoryTheory.MorphismProperty.instIsMonoidalInverseImageOfMonoidalOfRespectsIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [W.IsMonoidal] {C' : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_3, u_3} C'] [inst_4 : CategoryTheory.MonoidalCategory C']
  (F : CategoryTheory.Functor C' C) [F.Monoidal] [W.RespectsIso], (W.inverseImage F).IsMonoidal
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.natCast_eq_zero_iff_of_lt : ∀ {α : Type u_1} (p : ℕ) [inst : Lean.Grind.Semiring α] [Lean.Grind.IsCharP α p] {x : ℕ}, x < p → (↑x = 0 ↔ x = 0)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.mono : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν → ∀ (a : α), ∀ᵐ (b : β) ∂ν a, Monotone (f (a, b))
-- Mathlib.Topology.MetricSpace.Isometry
/-- **Alias** of `Isometry.preimage_setOfPred_dist`. -/
Isometry.preimage_setOf_dist : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (p : ℝ → Prop), f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}
-- Init.Control.Basic
instOrElseOfAlternative : (f : Type u → Type v) → (α : Type u) → [Alternative f] → OrElse (f α)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
_private.Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution.0.DiscreteConvolution.addFiber_swapEquiv : {M : Type u_1} →
  [inst : AddCommMonoid M] → (x : M) → ↑(DiscreteConvolution.addFiber x) ≃ ↑(DiscreteConvolution.addFiber x)
-- Std.Time.Date.PlainDate
/-- Transforms a `PlainDate` into a `Day.Ordinal.OfYear`.
 -/
Std.Time.PlainDate.dayOfYear : (date : Std.Time.PlainDate) → Std.Time.Day.Ordinal.OfYear date.year.isLeap