mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.TangentCone.Seq
/-- Auxiliary lemma ensuring that, under the assumptions from an old definition of the tangent cone,
the sequence `d` tends to 0 at infinity.  -/
tangentConeAt.lim_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {α : Type u_3} (l : Filter α) {c : α → 𝕜} {d : α → E} {y : E},
  Filter.Tendsto (fun n => ‖c n‖) l Filter.atTop →
    Filter.Tendsto (fun n => c n • d n) l (nhds y) → Filter.Tendsto d l (nhds 0)
-- Std.Data.DHashMap.Raw
/-- Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.DHashMap.Raw.filterMap : {α : Type u} →
  {β : α → Type v} → {γ : α → Type w} → ((a : α) → β a → Option (γ a)) → Std.DHashMap.Raw α β → Std.DHashMap.Raw α γ
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.add_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f₁ g₁ f₂ g₂ : C ⟶ D} (h₁ : Homotopy f₁ g₁) (h₂ : Homotopy f₂ g₂)
  (i j : ι), (h₁.add h₂).hom i j = h₁.hom i j + h₂.hom i j
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instAddGroup : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddGroup R] → AddGroup (HahnSeries Γ R)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre_nat : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal) (s : Set X),
  Filter.Tendsto (fun n => (MeasureTheory.OuterMeasure.mkMetric'.pre m (↑n)⁻¹) s) Filter.atTop
    (nhds ((MeasureTheory.OuterMeasure.mkMetric' m) s))
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseLeftKanExtension.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L L_1 : CategoryTheory.Functor C D) (e_L : L = L_1) (F F_1 : CategoryTheory.Functor C H) (e_F : F = F_1)
  [inst_3 : L.HasPointwiseLeftKanExtension F], L.pointwiseLeftKanExtension F = L_1.pointwiseLeftKanExtension F_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.cosh_le_cosh : ∀ {x y : ℝ}, Real.cosh x ≤ Real.cosh y ↔ |x| ≤ |y|
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- Representable presheaves are (trivially) ind-objects.  -/
CategoryTheory.Limits.IndObjectPresentation.yoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) → CategoryTheory.Limits.IndObjectPresentation (CategoryTheory.yoneda.obj X)
-- Lean.Elab.BuiltinCommand
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.innermostScopeName? : List Lean.Elab.Command.Scope → Option Lean.Name
-- Mathlib.Data.List.Sigma
List.dlookup_append : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l₁ l₂ : List (Sigma β)) (a : α),
  List.dlookup a (l₁ ++ l₂) = (List.dlookup a l₁).or (List.dlookup a l₂)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.map_injective : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β},
  Function.Injective f → Function.Injective fun M => M.map f
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_eq_iff_eq_castSucc : ∀ {n : ℕ} (i : Fin (n + 1)) (hi : i ≠ Fin.last n) (j : Fin n), i.castPred hi = j ↔ i = j.castSucc
-- Mathlib.LinearAlgebra.Dimension.Free
Module.nonempty_linearEquiv_iff_rank_eq_one : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], Nonempty (R ≃ₗ[R] M) ↔ Module.rank R M = 1
-- Batteries.Data.Vector.Basic
_private.Batteries.Data.Vector.Basic.0.Vector.scanrMFast.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} [inst : Monad m] (f : α → β → m β) (as : Vector α n)
  (cur : β) (i n_usize : USize) (h_n : n_usize.toNat = n) (h_i : i.toNat ≤ n) (acc : Vector β (n + 1)),
  Vector.scanrMFast.loop✝ f as cur i n_usize h_n h_i acc =
    if h_gt : 0 < i then
      have h_gt_nat := ⋯;
      let pred := i - 1;
      have h_pred := ⋯;
      do
      let next ← f (as.uget pred ⋯) cur
      Vector.scanrMFast.loop✝ f as next pred n_usize h_n ⋯ (acc.uset pred next ⋯)
    else pure acc
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_intCast : ∀ {R : Type u} [inst : Ring R] {n : ℤ}, Polynomial.derivative ↑n = 0
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.instSmallιAttachCellsιFunctorObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  [CategoryTheory.LocallySmall.{t, v, u} C] [Small.{t, w} I],
  Small.{t, max v w} (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).ι
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GMonoid.gnpowRec_zero : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMul A] [inst_2 : GradedMonoid.GOne A]
  (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (GradedMonoid.GMonoid.gnpowRec 0 a.snd) = 1
-- Mathlib.Topology.UniformSpace.Basic
Sum.uniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β],
  uniformity (α ⊕ β) =
    Filter.map (Prod.map Sum.inl Sum.inl) (uniformity α) ⊔ Filter.map (Prod.map Sum.inr Sum.inr) (uniformity β)
-- Mathlib.Order.Category.BoolAlg
typeToBoolAlgOp_obj : ∀ (X : Type u), typeToBoolAlgOp.obj X = Opposite.op { carrier := Set X, str := Set.instBooleanAlgebra }
-- Mathlib.Probability.HasLaw
/-- **Alias** of the forward direction of `ProbabilityTheory.indepFun_iff_hasLaw_prodMk_prod`. -/
ProbabilityTheory.IndepFun.hasLaw_prod : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {𝓨 : Type u_3}
  {m𝓨 : MeasurableSpace 𝓨} {ν : MeasureTheory.Measure 𝓨} {Y : Ω → 𝓨},
  ProbabilityTheory.HasLaw X μ P →
    ProbabilityTheory.HasLaw Y ν P →
      ProbabilityTheory.IndepFun X Y P → ProbabilityTheory.HasLaw (fun ω => (X ω, Y ω)) (μ.prod ν) P
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_eq_minimalPeriod_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {x : α} {g : β → β} {y : β},
  Function.minimalPeriod f x = Function.minimalPeriod g y ↔
    ∀ (n : ℕ), Function.IsPeriodicPt f n x ↔ Function.IsPeriodicPt g n y
-- Mathlib.LinearAlgebra.Prod
LinearMap.coe_snd : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], ⇑(LinearMap.snd R M M₂) = Prod.snd
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_filter_eq_size_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  {f : α → β → Bool} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.size = t.size ↔
    ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true),
      f (t.getKey a h) (Std.DTreeMap.Internal.Impl.Const.get t a h) = true
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.mem_singleton_set_smul : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] (N : Submodule R M) [SMulCommClass R S M] (r : S) (x : M),
  x ∈ {r} • N ↔ ∃ m ∈ N, x = r • m
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.fullyFaithfulToEssImage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful], F.toEssImage.IsEquivalence
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.overEquivOfIsInitial_counitIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.MorphismProperty.overEquivOfIsInitial.{w, v_1, u_1} P Q X h).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.Functor.fromPUnit
            (CategoryTheory.MorphismProperty.Over.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)).comp
        (CategoryTheory.Functor.star (P.Over Q X)))
-- Mathlib.Data.Nat.Log
_private.Mathlib.Data.Nat.Log.0.Nat.log.go.match_3.splitter : (motive : ℕ → ℕ → Sort u_1) → (x x_1 : ℕ) → ((x : ℕ) → motive x 0) → ((b fuel : ℕ) → motive b fuel.succ) → motive x x_1
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.zero : ∀ {G : Type u} [inst : AddGroup G] {B : AddGroupFilterBasis G} {U : Set G}, U ∈ B → 0 ∈ U
-- Init.Data.List.Lemmas
List.intercalate_singleton : ∀ {α : Type u_1} {ys xs : List α}, ys.intercalate [xs] = xs
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.neg : {α : Type u} → [Inv α] → Neg (Additive α)
-- Lean.Meta.FunInfo
/-- Update `hasFwdDeps` fields using new `backDeps`  -/
_private.Lean.Meta.FunInfo.0.Lean.Meta.updateHasFwdDeps : Array Lean.Meta.ParamInfo → Array ℕ → Array Lean.Meta.ParamInfo
-- Mathlib.Data.DFinsupp.Defs
/-- The function `single i b : Π₀ i, β i` sends `i` to `b`
and all other points to `0`.  -/
DFinsupp.single : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → [DecidableEq ι] → (i : ι) → β i → Π₀ (i : ι), β i
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instDecidableEqPurity : DecidableEq Lean.Compiler.LCNF.Purity
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumUniformlyOn.mono : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] {t : Set β}, HasSumUniformlyOn f g t → s ⊆ t → HasSumUniformlyOn f g s
-- Mathlib.Order.Monotone.Defs
Monotone.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  Monotone f = ∀ ⦃a b : α⦄, a ≤ b → f a ≤ f b
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F],
  CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G =
    CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G
-- Mathlib.CategoryTheory.Limits.MonoCoprod
/-- Given a family of objects `X : I₁ ⊕ I₂ → C`, a cofan of `X`, and two colimit cofans
of `X ∘ Sum.inl` and `X ∘ Sum.inr`, this is a cofan for `c₁.pt` and `c₂.pt` whose
point is `c.pt`.  -/
CategoryTheory.Limits.MonoCoprod.binaryCofanSum : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {I₁ : Type u_2} →
      {I₂ : Type u_3} →
        {X : I₁ ⊕ I₂ → C} →
          CategoryTheory.Limits.Cofan X →
            (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) →
              (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) →
                CategoryTheory.Limits.IsColimit c₁ →
                  CategoryTheory.Limits.IsColimit c₂ → CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt
-- Init.Data.Array.MapIdx
Array.mapFinIdx.eq_1 : ∀ {α : Type u} {β : Type v} (as : Array α) (f : (i : ℕ) → α → i < as.size → β),
  as.mapFinIdx f = (as.mapFinIdxM fun x1 x2 x3 => pure (f x1 x2 x3)).run
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.hom_homFromCommaOfIsIso : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X ⟶ Y)
  [inst_7 : CategoryTheory.IsIso (CategoryTheory.MorphismProperty.Comma.Hom.hom i)],
  CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso (CategoryTheory.MorphismProperty.Comma.Hom.hom i) = i
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.alls.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) →
      (x : ℕ) →
        (x_1 : L.BoundedFormula α x) →
          ((φ : L.BoundedFormula α 0) → motive 0 φ) →
            ((_n : ℕ) → (φ : L.BoundedFormula α (_n + 1)) → motive _n.succ φ) → motive x x_1
-- Mathlib.Algebra.Algebra.Tower
AlgHom.restrictScalars_apply : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A →ₐ[S] B) (x : A), (AlgHom.restrictScalars R f) x = f x
-- Lean.Util.FoldConsts
/-- Apply `f` to every constant occurring in `e` once.  -/
Lean.Expr.foldConsts : {α : Type} → Lean.Expr → α → (Lean.Name → α → α) → α
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.toMatrix_reindexEquiv : ∀ {n : Type u_1} {p : Type u_2} {R : Type u₂} [inst : DecidableEq n] [inst_1 : DecidableEq p] [inst_2 : CommRing R]
  [inst_3 : Fintype n] [inst_4 : Fintype p] (e : n ≃ p) (t : Matrix.TransvectionStruct n R),
  (Matrix.TransvectionStruct.reindexEquiv e t).toMatrix = (Matrix.reindexAlgEquiv R R e) t.toMatrix
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.Forall.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (x : α) (l : List α) (h_1 : Unit → motive []) (h_2 : (x : α) → motive [x])
  (h_3 : (x : α) → (l : List α) → motive (x :: l)),
  (l = [] → False) →
    (match x :: l with
      | [] => h_1 ()
      | [x] => h_2 x
      | x :: l => h_3 x l) =
      h_3 x l
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isSingular_iff : ∀ (c : Cardinal.{u_1}), c.IsSingular ↔ Cardinal.aleph0 ≤ c ∧ c.ord.cof ≠ c
-- Mathlib.Data.EReal.Basic
EReal.toReal_coe_ennreal : ∀ {x : ENNReal}, (↑x).toReal = x.toReal
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_add_of_nonpos : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R} {m n : ℤ}, m ≤ 0 → n ≤ 0 → A ^ (m + n) = A ^ m * A ^ n
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.Γgerm_res_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {FC : C → C → Type u_1} {CC : C → Type u_2} [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
  (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {i : U ⟶ ⊤} (x : ↑X) (hx : x ∈ U)
  [inst_3 : CategoryTheory.ConcreteCategory C FC] (s : CC (F.obj (Opposite.op ⊤))),
  (CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) ((CategoryTheory.ConcreteCategory.hom (F.map i.op)) s) =
    (CategoryTheory.ConcreteCategory.hom (F.Γgerm x)) s
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : Mul α] (w : m → α) (v : n → α) (i : m) (j : n),
  Matrix.vecMulVec w v i j = w i * v j
-- Batteries.Data.List.Lemmas
List.IsChain.cons_of_imp : ∀ {α : Type u_1} {R : α → α → Prop} {a : α} {l : List α} {b : α},
  (∀ (c : α), R a c → R b c) → List.IsChain R (a :: l) → List.IsChain R (b :: l)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.mono : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] [inst_1 : NormedAddCommGroup γ] {f : α → β} {g : α → γ},
  MeasureTheory.HasFiniteIntegral g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ ‖g a‖) → MeasureTheory.HasFiniteIntegral f μ
-- Init.Grind.AC
Lean.Grind.AC.Context.mk : {α : Sort u} → Lean.RArray (PLift α) → (α → α → α) → Lean.Grind.AC.Context α
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.withTopOrderIso.eq_1 : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  FiniteArchimedeanClass.withTopOrderIso M = WithTop.subtypeOrderIso
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.minView.congr_simp : ∀ {α : Type u} {β : α → Type v} (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced)
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size),
      Std.DTreeMap.Internal.Impl.minView k v l r hl hr hlr = Std.DTreeMap.Internal.Impl.minView k v_1 l r hl hr hlr
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.mk.sizeOf_spec : ∀ {V : Type u₁} [inst : Quiver V] {W : Type u₂} [inst_1 : Quiver W] [inst_2 : SizeOf V] [inst_3 : SizeOf W]
  (obj : V → W) (map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)), sizeOf { obj := obj, map := map } = 1
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_mul_left_add : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {x, z * x + y} = Ideal.span {x, y}
-- Std.Internal.UV.UDP
/-- Sets the membership for joining or leaving a multicast group. If `interfaceAddr` is `none`, the
default network interface is used.
 -/
Std.Internal.UV.UDP.Socket.setMembership : Std.Internal.UV.UDP.Socket → Std.Net.IPAddr → Option Std.Net.IPAddr → UInt8 → IO Unit
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`.  -/
TensorProduct : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      (N : Type u_8) →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid N] → [Module R M] → [Module R N] → Type (max u_7 u_8)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
/-- Bundles `fun x : ℝ≥0 => x ^ y` into an order isomorphism when `y : ℝ` is positive,
where the inverse is `fun x : ℝ≥0 => x ^ (1 / y)`.  -/
NNReal.orderIsoRpow : (y : ℝ) → 0 < y → NNReal ≃o NNReal
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
/-- The base case (0th coefficient) of our solution vector.  -/
WittVector.RecursionBase.solution : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] → {k : Type u_1} → [inst : Field k] → [IsAlgClosed k] → WittVector p k → WittVector p k → k
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toRingEquiv_opOp : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (AlgEquiv.opOp R A).toRingEquiv = RingEquiv.opOp A
-- Mathlib.Data.Set.Monotone
MonotoneOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  MonotoneOn f s → s₂ ⊆ s → MonotoneOn f s₂
-- Mathlib.Algebra.Group.End
AddAut.neg_def : ∀ (M : Type u_2) [inst : Add M] (e₁ : AddAut M), -e₁ = AddEquiv.symm e₁
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapCocycles₁_comp_i : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  CategoryTheory.CategoryStruct.comp (groupCohomology.mapCocycles₁ f φ)
      (groupCohomology.shortComplexH1 B).moduleCatLeftHomologyData.i =
    CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData.i
      (groupCohomology.cochainsMap₁ f φ)
-- Mathlib.Topology.Order.OrderClosed
interior_Iio : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a : α},
  interior (Set.Iio a) = Set.Iio a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_le_min?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k km kme : α}
  (hkme : (t.erase k).min? = some kme), t.min?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.Analysis.InnerProductSpace.MulOpposite
/-- The inner product of `Hᵐᵒᵖ` is given by `⟪x, y⟫ ↦ ⟪x.unop, y.unop⟫`.  -/
MulOpposite.instInner : {𝕜 : Type u_1} → {H : Type u_2} → [Inner 𝕜 H] → Inner 𝕜 Hᵐᵒᵖ
-- Lean.Data.KVMap
Lean.KVMap.setName : Lean.KVMap → Lean.Name → Lean.Name → Lean.KVMap
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Set.Finite.summable_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalAddGroup α]
  {f : β → α} {s : Set β}, s.Finite → (Summable (f ∘ Subtype.val) ↔ Summable f)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mapAlgEquiv_trans : ∀ {R : Type u} (σ : Type u_1) [inst : CommSemiring R] {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4}
  [inst_1 : CommSemiring A₁] [inst_2 : CommSemiring A₂] [inst_3 : CommSemiring A₃] [inst_4 : Algebra R A₁]
  [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃] (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃),
  (MvPolynomial.mapAlgEquiv σ e).trans (MvPolynomial.mapAlgEquiv σ f) = MvPolynomial.mapAlgEquiv σ (e.trans f)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Copy of an `OrderAddMonoidHom` with a new `toFun` equal to the old one. Useful to
fix definitional equalities.  -/
OrderAddMonoidHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : AddZeroClass α] → [inst_3 : AddZeroClass β] → (f : α →+o β) → (f' : α → β) → f' = ⇑f → α →+o β
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The map on valuation subrings to their unit groups is an order embedding.  -/
ValuationSubring.unitGroupOrderEmbedding : {K : Type u} → [inst : Field K] → ValuationSubring K ↪o Subgroup Kˣ
-- Batteries.Data.Array.Match
Array.Matcher.mk.inj : ∀ {α : Type u_1} {table : Array.PrefixTable α} {state : Fin (table.size + 1)} {table_1 : Array.PrefixTable α}
  {state_1 : Fin (table_1.size + 1)},
  { table := table, state := state } = { table := table_1, state := state_1 } → table = table_1 ∧ state ≍ state_1
-- Lean.Meta.Tactic.Grind.Action
Lean.Meta.Grind.Action.loop_skipIfNA : ∀ {n : ℕ} (a : Lean.Meta.Grind.Action),
  (Lean.Meta.Grind.Action.loopRef n a).skipIfNA = Lean.Meta.Grind.Action.loopRef n a
-- Init.Prelude
Nat.instMod : Mod ℕ
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_eq_bot_iff : ∀ (G : Type u_1) [inst : AddGroup G], addCommutator G = ⊥ ↔ IsAddCommutative G
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.mk.injEq : ∀ (keys : List Lean.Meta.RefinedDiscrTree.Key) (score : ℕ) (trie : Lean.Meta.RefinedDiscrTree.TrieIndex)
  (treeStars : Std.HashMap ℕ (List Lean.Meta.RefinedDiscrTree.Key)) (keys_1 : List Lean.Meta.RefinedDiscrTree.Key)
  (score_1 : ℕ) (trie_1 : Lean.Meta.RefinedDiscrTree.TrieIndex)
  (treeStars_1 : Std.HashMap ℕ (List Lean.Meta.RefinedDiscrTree.Key)),
  ({ keys := keys, score := score, trie := trie, treeStars := treeStars } =
      { keys := keys_1, score := score_1, trie := trie_1, treeStars := treeStars_1 }) =
    (keys = keys_1 ∧ score = score_1 ∧ trie = trie_1 ∧ treeStars = treeStars_1)
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_four : bernoulli' 4 = -1 / 30