mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.commute_mulLeft_right` for matrix multiplication.  -/
commute_mulLeftLinearMap_mulRightLinearMap : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_5} {A : Type u_6} [inst : Fintype m]
  [inst_1 : Fintype n] [inst_2 : CommSemiring R] [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A]
  [inst_5 : SMulCommClass R A A] [inst_6 : IsScalarTower R A A] (a : Matrix l m A) (b : Matrix n o A),
  mulLeftLinearMap o R a ∘ₗ mulRightLinearMap m R b = mulRightLinearMap l R b ∘ₗ mulLeftLinearMap n R a
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.mk : {V : Type u₁} →
  [inst : Quiver V] →
    {W : Type u₂} → [inst_1 : Quiver W] → (obj : V → W) → ({X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)) → V ⥤q W
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.mul_val_inv : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a), a * ↑h.unit⁻¹ = 1
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- A special case of `integral_Iic_of_hasDerivAt_of_tendsto` where we assume that `f` is C^1 with
compact support.  -/
HasCompactSupport.integral_Iic_deriv_eq : ∀ {E : Type u_1} {f : ℝ → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  ContDiff ℝ 1 f → HasCompactSupport f → ∀ (b : ℝ), ∫ (x : ℝ) in Set.Iic b, deriv f x = f b
-- Init.Data.SInt.Lemmas
Int16.toInt_maxValue : Int16.maxValue.toInt = 2 ^ 15 - 1
-- Mathlib.Tactic.Ring.Basic
/-- Turn coefficient data into a NormNum.Result.  -/
Mathlib.Tactic.Ring.RatCoeff.toResult : {u : Lean.Level} → {α : Q(Type u)} → {a : Q(«$α»)} → Mathlib.Tactic.Ring.RatCoeff a → Mathlib.Meta.NormNum.Result a
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.homEquiv_symm_apply_apply_apply : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {B : Type uB} [inst_2 : AddCommGroup B]
  [inst_3 : Module R A] [inst_4 : Module R B] (a : CharacterModule (TensorProduct R A B)) (x : A) (x_1 : B),
  ((CharacterModule.homEquiv.symm a) x) x_1 = a (x ⊗ₜ[R] x_1)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.tensorHom_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] {X₁ Y₁ X₂ Y₂ : P.FullSubcategory} (f : X₁ ⟶ Y₁)
  (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom)
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.Context.mk.inj : ∀ {elimInfo : Lean.Meta.ElimInfo} {targets : Array Lean.Expr} {elimInfo_1 : Lean.Meta.ElimInfo}
  {targets_1 : Array Lean.Expr},
  { elimInfo := elimInfo, targets := targets } = { elimInfo := elimInfo_1, targets := targets_1 } →
    elimInfo = elimInfo_1 ∧ targets = targets_1
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_inverse_obj : ∀ {J : Type u_1} {K : Type u_2} (x : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K),
  CategoryTheory.Discrete.sumEquiv.inverse.obj x =
    match x with
    | Sum.inl X => { as := Sum.inl X.as }
    | Sum.inr X => { as := Sum.inr X.as }
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF.measurable_measure_stieltjesFunction : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : ProbabilityTheory.IsMeasurableRatCDF f),
  Measurable fun a => (hf.stieltjesFunction a).measure
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.opFunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) {X Y : a ⟶ b} (η : X ⟶ Y),
  (Bicategory.Opposite.opFunctor a b).map η = Bicategory.Opposite.op2 η
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.atIdx?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.Equiv t₂ → t₁.atIdx? i = t₂.atIdx? i
-- Mathlib.Data.Fin.Tuple.Basic
Fin.range_fin_succ : ∀ {n : ℕ} {α : Type u_1} (f : Fin (n + 1) → α), Set.range f = insert (f 0) (Set.range (Fin.tail f))
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.le_div : ∀ {a b c : Ordinal.{u_4}}, c ≠ 0 → (a ≤ b / c ↔ c * a ≤ b)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLTHAddIntOfNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (X : C) (n : ℤ), t.IsLE ((t.truncLT (n + 1)).obj X) n
-- Lean.Expr
/-- Implicit binder annotation, e.g., `{x : α}`  -/
Lean.BinderInfo.implicit : Lean.BinderInfo
-- Mathlib.Algebra.Order.Field.Basic
one_div_lt : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → 0 < b → (1 / a < b ↔ 1 / b < a)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.congrHom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f₁ f₂ : X ⟶ Y} {g₁ g₂ : X ⟶ Z} (h₁ : f₁ = f₂)
  (h₂ : g₁ = g₂) [inst_1 : CategoryTheory.Limits.HasPushout f₁ g₁] [inst_2 : CategoryTheory.Limits.HasPushout f₂ g₂],
  (CategoryTheory.Limits.pushout.congrHom h₁ h₂).hom =
    CategoryTheory.Limits.pushout.map f₁ g₁ f₂ g₂ (CategoryTheory.CategoryStruct.id Y)
      (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.tendsto_setIntegral_of_antitone : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [inst_2 : Preorder ι] [Filter.atTop.IsCountablyGenerated]
  {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Antitone s →
      (∃ i, MeasureTheory.IntegrableOn f (s i) μ) →
        Filter.Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) Filter.atTop (nhds (∫ (x : X) in ⋂ n, s n, f x ∂μ))
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X} [inst_1 : SizeOf C]
  (toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂) (c : CategoryTheory.Limits.PullbackCone p₂ p₁)
  (isLimit : CategoryTheory.Limits.IsLimit c) (t : c.pt ⟶ R)
  (transitivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam)
  (transitivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam),
  sizeOf
      { toJointlyMono₂ := toJointlyMono₂, c := c, isLimit := isLimit, t := t, transitivity₁ := transitivity₁,
        transitivity₂ := transitivity₂ } =
    1 + sizeOf toJointlyMono₂ + sizeOf c + sizeOf isLimit + sizeOf t + sizeOf transitivity₁ + sizeOf transitivity₂
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.elabImplicitLambda : Lean.Syntax → Bool → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.copyCount_eq_card_image_copyToSubgraph : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : Fintype { f // Function.Injective ⇑f }] [inst_2 : DecidableEq G.Subgraph],
  G.copyCount H = (Finset.image SimpleGraph.Copy.toSubgraph Finset.univ).card
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.mul_smul : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] (x y : OreLocalization S R) (z : OreLocalization S X), (x * y) • z = x • y • z
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- Given functors `F₁` and `F₂` in `J ⥤ C`, where `C` is a category enriched in `V`,
this condition allows the definition of `functorEnrichedHom V F₁ F₂ : J ⥤ V`.  -/
CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [CategoryTheory.EnrichedOrdinaryCategory V C] →
                CategoryTheory.Functor J C → CategoryTheory.Functor J C → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- If `C` is a small finitely cocomplete category and `A : Cᵒᵖ ⥤ Type u` is a presheaf such that
`CostructuredArrow yoneda A` is filtered, then `A` preserves finite limits.

One direction of Proposition 3.3.13 of [Kashiwara2006].
 -/
CategoryTheory.Limits.preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type u))
  [CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)],
  CategoryTheory.Limits.PreservesFiniteLimits A
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- Given a functor `K : J ⥤ Over X` and its extension `liftFromOver K : WithTerminal J ⥤ C`,
there is an obvious equivalence between cones of these two functors.
A cone of `K` is an object of `Over X`, so it has the form `t ⟶ X`.
Equivalently, a cone of `WithTerminal K` is an object `t : C`,
and we can recover the structure morphism as `π.app X : t ⟶ X`.  -/
CategoryTheory.WithTerminal.coneEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Over X)} →
            CategoryTheory.Limits.Cone K ≌ CategoryTheory.Limits.Cone (CategoryTheory.WithTerminal.liftFromOver.obj K)
-- Mathlib.MeasureTheory.Measure.LevyConvergence
/-- If the characteristic functions of a sequence of probability measures converge pointwise to
the characteristic function of a probability measure, then the measures converge weakly.  -/
MeasureTheory.ProbabilityMeasure.tendsto_of_tendsto_charFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ₀ : MeasureTheory.ProbabilityMeasure E}
  {μ : ℕ → MeasureTheory.ProbabilityMeasure E},
  (∀ (t : E),
      Filter.Tendsto (fun n => MeasureTheory.charFun (↑(μ n)) t) Filter.atTop (nhds (MeasureTheory.charFun (↑μ₀) t))) →
    Filter.Tendsto μ Filter.atTop (nhds μ₀)
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeAddSemigroup.toFreeAddMonoid.eq_1 : ∀ {α : Type u_1}, FreeAddSemigroup.toFreeAddMonoid = FreeAddSemigroup.lift FreeAddMonoid.of
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : Group E] [inst_2 : SeminormedGroup F]
  [inst_3 : MonoidHomClass 𝓕 E F] (f : 𝓕),
  SeminormedGroup.induced E F f =
    { norm := fun a => ‖f a‖, toGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.Order.Hom.Bounded
/-- The underlying function. The preferred spelling is `DFunLike.coe`.  -/
TopHom.toFun : {α : Type u_6} → {β : Type u_7} → [inst : Top α] → [inst_1 : Top β] → TopHom α β → α → β
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.Sheaf.isSeparated : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {J : CategoryTheory.GrothendieckTopology C} {FA : A → A → Type u_1} {CA : A → Type u_2}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [J.HasSheafCompose (CategoryTheory.forget A)] (F : CategoryTheory.Sheaf J A),
  CategoryTheory.Presheaf.IsSeparated J F.obj
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_finsetProd : ∀ {ι : Type u_1} {S : Type u_2} [inst : Add S] [inst_1 : CommMonoid S] (t : RingCon S) (s : Finset ι) (f : ι → S),
  ↑(s.prod f) = ∏ i ∈ s, ↑(f i)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_ne_top : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R}, x.orderTop ≠ ⊤ ↔ x ≠ 0
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
/-- **Triangle inequality** for angles between vectors.  -/
InnerProductGeometry.angle_le_angle_add_angle : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y z : V),
  InnerProductGeometry.angle x z ≤ InnerProductGeometry.angle x y + InnerProductGeometry.angle y z
-- Mathlib.Analysis.Fourier.AddCircleMulti
AddCircle.haarAddCircle.eq_1 : ∀ {T : ℝ} [hT : Fact (0 < T)], AddCircle.haarAddCircle = MeasureTheory.Measure.addHaarMeasure ⊤
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.sieves_copy : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {s : (X : C) → Set (CategoryTheory.Sieve X)} {h : J.sieves = s}, (J.copy s h).sieves = s
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minKey?_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)}, Std.Internal.List.containsKey k l = true → (Std.Internal.List.minKey? l).isSome = true
-- Mathlib.CategoryTheory.Sites.GlobalSections
CategoryTheory.Sheaf.ΓRes_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A]
  [inst_3 : CategoryTheory.HasGlobalSectionsFunctor J A] (F : CategoryTheory.Sheaf J A) {V U : Cᵒᵖ} (f : U ⟶ V) {Z : A}
  (h : F.obj.obj V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.ΓRes U) (CategoryTheory.CategoryStruct.comp (F.obj.map f) h) =
    CategoryTheory.CategoryStruct.comp (F.ΓRes V) h
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.comp.congr_simp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} {φ : M → N} {ψ : N → P} {χ : M → P} {X : Type u_5} [inst : SMul M X]
  {Y : Type u_6} [inst_1 : SMul N Y] {Z : Type u_7} [inst_2 : SMul P Z] (g g_1 : Y →ₑ[ψ] Z),
  g = g_1 → ∀ (f f_1 : X →ₑ[φ] Y), f = f_1 → ∀ [κ : CompTriple φ ψ χ], g.comp f = g_1.comp f_1
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.instMulCauchy : {α : Type u_1} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] →
      [inst_2 : IsStrictOrderedRing α] →
        {β : Type u_2} →
          [inst_3 : Ring β] → {abv : β → α} → [inst_4 : IsAbsoluteValue abv] → Mul (CauSeq.Completion.Cauchy abv)
-- Mathlib.Order.KrullDimension
Order.height_int : ∀ (n : ℤ), Order.height n = ⊤
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs
Matrix.trace_eq_sum_roots_charpoly_of_splits : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R] {B : Matrix n n R}
  [inst_3 : IsDomain R], B.charpoly.Splits → B.trace = B.charpoly.roots.sum
-- Mathlib.CategoryTheory.Functor.Trifunctor
CategoryTheory.bifunctorComp₂₃_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₂₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) (X₁ : C₁),
  (CategoryTheory.bifunctorComp₂₃ F G₂₃).obj X₁ = CategoryTheory.bifunctorComp₂₃Obj F G₂₃ X₁
-- Mathlib.Control.Bitraversable.Basic
/-- Lawless bitraversable bifunctor. This only holds data for the bimap and bitraverse.  -/
Bitraversable : (Type u → Type u → Type u) → Type (u + 1)
-- Mathlib.Data.Nat.Basic
Nat.mul_le_pow : ∀ {a : ℕ}, a ≠ 1 → ∀ (b : ℕ), a * b ≤ a ^ b
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.rescale_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (f : ℕ → R) (a : R),
  (PowerSeries.rescale a) (PowerSeries.mk f) = PowerSeries.mk fun n => a ^ n * f n
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapRange.linearMap_id : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.mapRange.linearMap LinearMap.id = LinearMap.id
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.realize_sum : ∀ {α : Type u_1} {M : Type u_2} {v : α → M} [inst : AddCommMonoidWithOne M] {β : Type u_3} {s : Finset β}
  {f : β → FirstOrder.Language.presburger.Term α},
  FirstOrder.Language.Term.realize v (FirstOrder.Language.presburger.sum s f) =
    ∑ i ∈ s, FirstOrder.Language.Term.realize v (f i)
-- Init.Data.Array.Int
Array.sum_div_length_le_max_int : ∀ {xs : Array ℤ} (h : xs ≠ #[]), xs.sum / ↑xs.size ≤ xs.max h
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Inhabited α] [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.mk.inj : ∀ {map map_1 : Lean.AssocList Lean.FVarId Lean.Expr}, { map := map } = { map := map_1 } → map = map_1
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condIndep_biSup_limsup : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {p : Set ι → Prop} {f : Filter ι} [inst : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        ∀ {t : Set ι}, p t → ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) (Filter.limsup s f) hm μ
-- Std.Data.HashMap.Basic
Std.HashMap.mk : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (Std.DHashMap α fun x => β) → Std.HashMap α β
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] (a b : ℝ) (f : ι → Ω → ℝ)
  (N : ι) (ω : Ω),
  MeasureTheory.upcrossingsBefore a b f N ω = sSup {n | MeasureTheory.upperCrossingTime a b f N n ω < N}
-- Std.Async.Basic
Std.Async.EAsync.instMonadAwaitTask : {ε : Type} → Std.Async.MonadAwait Task (Std.Async.EAsync ε)
-- Mathlib.Data.Finsupp.Order
/-- This is called `tsub` for truncated subtraction, to distinguish it with subtraction in an
additive group.  -/
Finsupp.tsub : {ι : Type u_1} →
  {α : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → [inst_3 : Sub α] → [OrderedSub α] → Sub (ι →₀ α)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.inter_left : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → ∀ (X : Set α), M.Indep (X ∩ I)
-- Mathlib.Tactic.Ring.Basic
/-- Negate rational number expressions.  -/
Mathlib.Tactic.Ring.RingCompute.neg : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a : Q(«$α»)} →
      (_crα : Q(CommRing «$α»)) →
        Mathlib.Tactic.Ring.RatCoeff a →
          Lean.MetaM (Mathlib.Tactic.Ring.Common.Result Mathlib.Tactic.Ring.RatCoeff q(-«$a»))
-- Mathlib.Topology.ContinuousOn
isOpenMap_prod_of_discrete_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ},
  IsOpenMap f ↔ ∀ (b : β), IsOpenMap fun x => f (x, b)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dotId.inj : ∀ {stx : Lean.Syntax} {id : Lean.Name} {lctx : Lean.LocalContext} {expectedType? : Option Lean.Expr}
  {stx_1 : Lean.Syntax} {id_1 : Lean.Name} {lctx_1 : Lean.LocalContext} {expectedType?_1 : Option Lean.Expr},
  Lean.Elab.CompletionInfo.dotId stx id lctx expectedType? =
      Lean.Elab.CompletionInfo.dotId stx_1 id_1 lctx_1 expectedType?_1 →
    stx = stx_1 ∧ id = id_1 ∧ lctx = lctx_1 ∧ expectedType? = expectedType?_1
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_mapComp_inv_toNatTrans_app : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] {a b c : CategoryTheory.Cat} (x : a ⟶ b) (x_1 : b ⟶ c)
  (X : CategoryTheory.Join (↑a) D),
  ((CategoryTheory.Join.pseudofunctorLeft D).mapComp x x_1).inv.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Join.mapPairComp x.toFunctor (CategoryTheory.Functor.id D) x_1.toFunctor
              (CategoryTheory.Functor.id D)).inv.app
        X)
      (match X with
      | CategoryTheory.Join.left x_2 =>
        CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (x_1.toFunctor.obj (x.toFunctor.obj x_2)))
      | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x))
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_eq_trim_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ : MeasureTheory.OuterMeasure α},
  m₁.trim = m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s = m₂ s
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedFnBody.default_1 : Lean.IR.FnBody
-- Mathlib.Order.Filter.Subsingleton
Filter.Subsingleton.anti : ∀ {α : Type u_1} {l l' : Filter α}, l.Subsingleton → l' ≤ l → l'.Subsingleton
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.projectLeftAssign.eq_1 : ∀ (aig : Std.Sat.AIG ℕ) (assign : ℕ → Bool) (var : ℕ),
  Std.Sat.AIG.toCNF.projectLeftAssign✝ aig assign var = assign (var + aig.decls.size)
-- Batteries.Recycling.RBTree.Basic
/-- The actual well-formedness invariant: a red-black tree has the
ordering and balance invariants.  -/
RBTree.RBNode.WF.mk : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : RBTree.RBNode α} {c : RBTree.RBColor} {n : ℕ},
  RBTree.RBNode.Ordered cmp t → t.Balanced c n → RBTree.RBNode.WF cmp t
-- Init.Data.List.Find
List.findIdx_of_getElem?_eq_some : ∀ {α : Type u_1} {p : α → Bool} {y : α} {xs : List α}, xs[List.findIdx p xs]? = some y → p y = true
-- Mathlib.SetTheory.Cardinal.Embedding
Fin.Embedding.exists_embedding_disjoint_range_of_add_le_Nat_card : ∀ {α : Type u_1} {n : ℕ} {s : Set α} [Finite α], s.ncard + n ≤ Nat.card α → ∃ y, Disjoint s (Set.range ⇑y)
-- Init.Data.List.Perm
List.countP_eq_countP_filter_add : ∀ {α : Type u_1} (l : List α) (p q : α → Bool),
  List.countP p l = List.countP p (List.filter q l) + List.countP p (List.filter (fun a => !q a) l)
-- Init.Data.UInt.Basic
/-- Bitwise or for 64-bit unsigned integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.lor : UInt64 → UInt64 → UInt64
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TacticNode.mk.sizeOf_spec : ∀ (ctxI : Lean.Elab.ContextInfo) (tacI : Lean.Elab.TacticInfo) (mayFail : Bool),
  sizeOf { ctxI := ctxI, tacI := tacI, mayFail := mayFail } = 1 + sizeOf ctxI + sizeOf tacI + sizeOf mayFail