mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.mk.sizeOf_spec : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} [inst_3 : SizeOf C₁] [inst_4 : SizeOf C₂]
  [inst_5 : SizeOf C₃] (adj : (X₁ : C₁) → F.obj X₁ ⊣ G.obj (Opposite.op X₁))
  (unit_whiskerRight_map :
    autoParam
      (∀ {X₁ Y₁ : C₁} (f : X₁ ⟶ Y₁),
        CategoryTheory.CategoryStruct.comp (adj X₁).unit
            (CategoryTheory.Functor.whiskerRight (F.map f) (G.obj (Opposite.op X₁))) =
          CategoryTheory.CategoryStruct.comp (adj Y₁).unit ((F.obj Y₁).whiskerLeft (G.map f.op)))
      CategoryTheory.ParametrizedAdjunction.unit_whiskerRight_map._autoParam),
  sizeOf { adj := adj, unit_whiskerRight_map := unit_whiskerRight_map } = 1
-- Mathlib.Tactic.Translate.Reorder
/-- Apply the given binder infos to the binders in expression `e`.  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.fixBinderInfos : List Lean.BinderInfo → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBy.mk_ideal_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (a b : R)
  (x : ↥(Submodule.torsionBy R M a)), (Ideal.Quotient.mk (Ideal.span {a})) b • x = b • x
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.ind_rec : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g₁ g₂ : MvQPF.Fix F α → β),
  (∀ (x : F (α ::: MvQPF.Fix F α)),
      MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (TypeVec.id ::: g₂) x →
        g₁ (MvQPF.Fix.mk x) = g₂ (MvQPF.Fix.mk x)) →
    ∀ (x : MvQPF.Fix F α), g₁ x = g₂ x
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.IsElliptic.c_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [IsOrderedRing R] {m : Matrix (Fin 2) (Fin 2) R},
  m.IsElliptic → m 1 0 ≠ 0
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.toTupleMvPolynomial.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R),
  p.toTupleMvPolynomial = ![p.homogenize p.natDegree, MvPolynomial.X 1 ^ p.natDegree]
-- Mathlib.Algebra.Group.Defs
inv_eq_one_div : ∀ {G : Type u_1} [inst : DivInvMonoid G] (x : G), x⁻¹ = 1 / x
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- `M.map f` is the matrix obtained by applying `f` to each entry of the matrix `M`.

This is available in bundled forms as:
* `AddMonoidHom.mapMatrix`
* `LinearMap.mapMatrix`
* `RingHom.mapMatrix`
* `AlgHom.mapMatrix`
* `Equiv.mapMatrix`
* `AddEquiv.mapMatrix`
* `LinearEquiv.mapMatrix`
* `RingEquiv.mapMatrix`
* `AlgEquiv.mapMatrix`
 -/
Matrix.map : {m : Type u_2} → {n : Type u_3} → {α : Type v} → {β : Type w} → Matrix m n α → (α → β) → Matrix m n β
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.opEquiv_apply : ∀ {X : SSet} {A : X.Subcomplex} (x : A.op.N), SSet.Subcomplex.N.opEquiv x = { toN := SSet.N.opEquiv x.toN, notMem := ⋯ }
-- Mathlib.NumberTheory.ADEInequality
/-- `sumInv pqr` for a `pqr : Multiset ℕ+` is the sum of the inverses
of the elements of `pqr`, as rational number.

The intended argument is a multiset `{p,q,r}` of cardinality `3`.  -/
ADEInequality.sumInv : Multiset ℕ+ → ℚ
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.one_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R), 1 * φ = φ
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero_aux1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E),
  Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
      (nhds 0) →
    ∀ (t u : Set E),
      μ u ≠ 0 →
        t ⊆ Metric.closedBall 0 1 →
          Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.toPreAbstractSimplicialComplex_lt_iff : ∀ {ι : Type u_1} {K L : AbstractSimplicialComplex ι},
  K.toPreAbstractSimplicialComplex < L.toPreAbstractSimplicialComplex ↔ K < L
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey! k = default
-- Lean.Expr
/-- Similar to `Lean.Expr.instantiateRev`, but considers only the substitutions `subst` in the range `[beginIdx, endIdx)`.
Function panics if `beginIdx <= endIdx <= subst.size` does not hold.

This function is equivalent to `instantiateRev e (subst.extract beginIdx endIdx)`, but it does not allocate a new array.

This instantiates with the "forwards" indexing scheme (see the docstring for `Lean.Expr.instantiateRev` for an example).
See also `Lean.Expr.instantiateRange`, which instantiates with the "backwards" indexing scheme.
 -/
Lean.Expr.instantiateRevRange : Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_eq : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.X = (PowerSeries.monomial 1) 1
-- Mathlib.Algebra.Quandle
/-- Proof of left inverse  -/
Rack.left_inv : ∀ {α : Type u} [self : Rack α] (x : α), Function.LeftInverse (Rack.invAct x) (Shelf.act x)
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.mem_ofPolynomial : ∀ {R : Type u} [inst : Semiring R] {I : Ideal (Polynomial R)} (x : Polynomial R), x ∈ I.ofPolynomial ↔ x ∈ I
-- Init.Data.UInt.Lemmas
UInt16.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 16 → b < 2 ^ 16 → UInt16.ofNat (a % b) = UInt16.ofNat a % UInt16.ofNat b
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.Integrable.summable_integral : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {μ : ι → MeasureTheory.Measure X} {f : X → E},
  MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) → Summable fun i => ∫ (x : X), ‖f x‖ ∂μ i
-- Init.Data.Array.Extract
Array.set_extract : ∀ {α : Type u_1} {as : Array α} {i j k : ℕ} (h : k < (as.extract i j).size) {a : α},
  (as.extract i j).set k a h = (as.set (i + k) a ⋯).extract i j
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.isoMk_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A B : CategoryTheory.Pretriangulated.Triangle C) (iso₁ : A.obj₁ ≅ B.obj₁) (iso₂ : A.obj₂ ≅ B.obj₂)
  (iso₃ : A.obj₃ ≅ B.obj₃)
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom B.mor₁)
      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp A.mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom B.mor₂)
      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp A.mor₃ ((CategoryTheory.shiftFunctor C 1).map iso₁.hom) =
        CategoryTheory.CategoryStruct.comp iso₃.hom B.mor₃)
      CategoryTheory.Pretriangulated.Triangle.isoMk._auto_5),
  (A.isoMk B iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).hom = A.homMk B iso₁.hom iso₂.hom iso₃.hom comm₁ comm₂ comm₃
-- Mathlib.Topology.Separation.Hausdorff
Filter.limUnder_eq_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] {f : Filter Y} [f.NeBot] {g : Y → X},
  (∃ x, Filter.Tendsto g f (nhds x)) → ∀ {x : X}, f.limUnder g = x ↔ Filter.Tendsto g f (nhds x)
-- Mathlib.GroupTheory.Congruence.Basic
Con.submonoid.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (c : Con M), ↑c = { carrier := {x | c x.1 x.2}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.zero_apply : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_5} (F : FormalGroup R), ↑0 = 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.map_zero : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S),
  AddMonoidAlgebra.map f 0 = 0
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActions.mk : Array Lean.CodeAction.CommandCodeAction →
  Lean.NameMap (Array Lean.CodeAction.CommandCodeAction) → Lean.CodeAction.CommandCodeActions
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.IsInner.ne_zero : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {inst : P.IsProper} [self : P.IsInner] (x : ↑P.II) {d : ℕ}
  (hd : (↑x).dim = d), ⋯.index hd ≠ 0
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.OplaxFunctor.mapComp'_comp_whiskerLeft_mapComp' : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f),
  CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯)
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃)) =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂) (F.map f₂₃))
        (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom)
-- Lean.Elab.App
/-- Add the given metavariable to the collection of metavariables associated with instance-implicit arguments.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.addInstMVar : Lean.MVarId → Lean.Elab.Term.ElabAppArgs.M Unit
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
ContMDiffMap.mdifferentiable' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : ContMDiffMap I I' M M' n),
  n ≠ 0 → MDiff ⇑f
-- Init.Data.Int.Gcd
Int.dvd_lcm_right : ∀ (a b : ℤ), b ∣ ↑(a.lcm b)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.instAddOpposite : ∀ {G : Type u} [inst : Add G] [h : UniqueSums G], UniqueSums Gᵃᵒᵖ
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorIdSearchStepOfBackwardPattern.match_3.splitter : {ρ : Type} →
  (pat : ρ) →
    (s : String.Slice) →
      (it : Std.IterM Id (String.Slice.Pattern.SearchStep s)) →
        (motive : Option (s.sliceTo it.internalState.currPos).Pos → Sort u_1) →
          (x : Option (s.sliceTo it.internalState.currPos).Pos) →
            ((pos : (s.sliceTo it.internalState.currPos).Pos) → x = some pos → motive (some pos)) →
              (x = none → motive none) → motive x
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntry!_eq_getEntry! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} [inst_4 : Inhabited ((a : α) × β a)],
      m.getEntry! a = Std.Internal.List.getEntry! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Batteries.Data.List.Lemmas
List.diff.eq_2 : ∀ {α : Type u_1} [inst : BEq α] (x : List α) (a : α) (l₂ : List α),
  x.diff (a :: l₂) = if List.elem a x = true then (x.erase a).diff l₂ else x.diff l₂
-- Lean.Parser.Extra
Lean.Parser.withOpenDecl.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.distinct_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.toList
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- If `f` has a derivative at `x` within `s`, then `fderivWithin 𝕜 f s x` is such a derivative.
Otherwise, it is set to `0`. We also set it to be zero, if zero is one of possible derivatives.  -/
fderivWithin : (𝕜 : Type u_4) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_5} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : TopologicalSpace E] →
            {F : Type u_6} →
              [inst_4 : AddCommGroup F] →
                [inst_5 : Module 𝕜 F] → [inst_6 : TopologicalSpace F] → (E → F) → Set E → E → E →L[𝕜] F
-- Mathlib.LinearAlgebra.FixedSubmodule
/-- When `u : V ≃ₗ[R] V` maps a submodule `W` into itself,
this is the induced linear equivalence of `V ⧸ W`, as a group homomorphism.  -/
LinearEquiv.reduce : {R : Type u_4} →
  {V : Type u_5} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module R V] → (W : Submodule R V) → ↥(MulAction.stabilizer (V ≃ₗ[R] V) W) →* (V ⧸ W) ≃ₗ[R] V ⧸ W
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Triangle.equilateral_iff_dist_eq_and_dist_eq : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {t : Affine.Triangle R P}
  {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        (Affine.Simplex.Equilateral t ↔
          dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
            dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃))
-- Init.LawfulBEqTactics
tacticDeriving_LawfulEq_tactic : Lean.ParserDescr
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.add_eq_le : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α],
  a₁ = b₁ → a₂ ≤ b₂ → a₁ + a₂ ≤ b₁ + b₂
-- Mathlib.Geometry.Manifold.IsManifold.Basic
contDiffGroupoid.eq_1 : ∀ (n : WithTop ℕ∞) {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  contDiffGroupoid n I = (contDiffPregroupoid n I).groupoid
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_eq_comap_nhds_zero : ∀ (Gᵣ : Type u_3) [inst : UniformSpace Gᵣ] [inst_1 : AddGroup Gᵣ] [IsRightUniformAddGroup Gᵣ],
  uniformity Gᵣ = Filter.comap (fun x => x.2 - x.1) (nhds 0)
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom_mop_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f.mop g =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom g f
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceShiftLeft : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Normed.Ring.Basic
norm_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedCommRing α] [NormMulClass α] [NormOneClass α] (s : Finset β)
  (f : β → α), ‖∏ b ∈ s, f b‖ = ∏ b ∈ s, ‖f b‖
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.fix.sizeOf_spec : ∀ (a : Turing.ToPartrec.Code) (a_1 : Turing.ToPartrec.Cont),
  sizeOf (Turing.ToPartrec.Cont.fix a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_apply' : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ℝ) {s : Set α},
  MeasurableSet s → (μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (Real.exp (f a) / ∫ (x : α), Real.exp (f x) ∂μ) ∂μ
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.rightUnitor_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X : P.FullSubcategory),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor X =
    P.isoMk (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.obj)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.add_nfBelow : ∀ {b : Ordinal.{0}} {o₁ o₂ : ONote}, o₁.NFBelow b → o₂.NFBelow b → (o₁ + o₂).NFBelow b
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurry_curryRight : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G),
  f.curryRight.uncurryRight = f
-- Mathlib.Order.SuccPred.Archimedean
WellFoundedLT.toIsPredArchimedean : ∀ {α : Type u_1} [inst : PartialOrder α] [h : WellFoundedLT α] [inst_1 : PredOrder α], IsPredArchimedean α
-- Mathlib.Tactic.Translate.Reorder
/-- Reorder the arguments of a function using the given `ArgReorder`.  -/
Mathlib.Tactic.Translate.reorderLambda : Mathlib.Tactic.Translate.ArgReorder → Lean.Expr → Lean.MetaM Lean.Expr
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Raw.any.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β) (p : (a : α) → β a → Bool),
  m.any p =
    (do
        let __s ←
          forIn m (none, ()) fun a __s =>
              if p a.fst a.snd = true then pure (ForInStep.done (some true, ())) else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure false).run
-- Mathlib.Data.Finset.Insert
Finset.singleton_iff_unique_mem : ∀ {α : Type u_1} (s : Finset α), (∃ a, s = {a}) ↔ ∃! a, a ∈ s
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_functor_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ)
  {X Y : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ} (f : X ⟶ Y) (x : Fin (n + 1)),
  ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.map f).app x = (f.unop.app x.rev).op
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.indep_iff_forall_notMem_closure_sdiff : ∀ {α : Type u_2} {M : Matroid α} {I : Set α},
  autoParam (I ⊆ M.E) Matroid.indep_iff_forall_notMem_closure_sdiff._auto_1 →
    (M.Indep I ↔ ∀ ⦃e : α⦄, e ∈ I → e ∉ M.closure (I \ {e}))
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : Mul M], Subsemigroup.instInhabited = { default := ⊥ }
-- Mathlib.NumberTheory.WellApproximable
mem_approxOrderOf_iff : ∀ {A : Type u_1} [inst : SeminormedGroup A] {n : ℕ} {δ : ℝ} {a : A},
  a ∈ approxOrderOf A n δ ↔ ∃ b, orderOf b = n ∧ a ∈ Metric.ball b δ
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.dvd_gcd : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {a : α}, (∀ b ∈ s, a ∣ f b) → a ∣ s.gcd f
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_lt_top_of_finite : ∀ {α : Type u_1} [Finite α], ENat.card α < ⊤
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_le_ofBoolRing_iff : ∀ {α : Type u_1} [inst : BooleanAlgebra α] {a b : AsBoolRing α}, ofBoolRing a ≤ ofBoolRing b ↔ a * b = a
-- Lean.Data.OpenDecl
Lean.OpenDecl.explicit.injEq : ∀ (id declName id_1 declName_1 : Lean.Name),
  (Lean.OpenDecl.explicit id declName = Lean.OpenDecl.explicit id_1 declName_1) = (id = id_1 ∧ declName = declName_1)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_of_mem_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E},
  s ∈ nhds x → VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracket 𝕜 V W x
-- Mathlib.Data.Vector.Basic
List.Vector.get_map₂ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (v₁ : List.Vector α n) (v₂ : List.Vector β n) (f : α → β → γ)
  (i : Fin n), (List.Vector.map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)
-- Lean.Meta.Tactic.NormCast
/-- Counts how many coercions are at the head of the expression.  -/
Lean.Meta.NormCast.countHeadCoes : Lean.Expr → Lean.MetaM ℕ
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to infinity along a filter, then `f` multiplied by a positive
constant (on the left) also tends to infinity. For a version working in `ℕ` or `ℤ`, use
`Filter.Tendsto.const_mul_atTop'` instead.  -/
Filter.Tendsto.const_mul_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => r * f x) l Filter.atTop
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instIsCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsCancelAdd α], IsCancelAdd αᵒᵈ
-- Lean.Message
/-- Returns the string-formatted version of MessageData.

Note: this is a potentially expensive operation that is only relevant to message data that are
actually rendered. Consider using this function in lazy message data to avoid unnecessary
computation for messages that are not displayed.
 -/
_private.Lean.Message.0.Lean.MessageData.formatExpensively : Lean.PPContext → Lean.MessageData → BaseIO String
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.mulActionBaseChange_smul_add : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A] (a : A) (x y : TensorProduct R S Ω[A⁄R]), a • (x + y) = a • x + a • y
-- Mathlib.Order.Filter.Pointwise
Filter.Tendsto.sub_sub : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β},
  Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) g₁ g₂ → Filter.Tendsto (⇑m) (f₁ - g₁) (f₂ - g₂)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- A version of `measurable_sub_const` that assumes `MeasurableAdd` instead of
`MeasurableSub`. This can be nice to avoid unnecessary type-class assumptions.  -/
measurable_sub_const' : ∀ {G : Type u_2} [inst : SubNegMonoid G] [inst_1 : MeasurableSpace G] [MeasurableAdd G] (g : G),
  Measurable fun h => h - g
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderType.parenthesizer : optParam Bool false → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Any.eq_1 : ∀ {α : Type u_1} (P : α → Prop), Ordnode.Any P Ordnode.nil = False
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming
Tactic.ComputeAsymptotics.MultiseriesExpansion.IsZero.approximates_zero : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion basis},
  ms.IsZero → ms.Approximates → ms.toFun =ᶠ[Filter.atTop] 0
-- Init.Data.AC
Lean.Data.AC.eval : {α : Sort u_1} → (β : Sort u) → [Lean.Data.AC.EvalInformation α β] → α → Lean.Data.AC.Expr → β
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.nilradical.eq_1 : ∀ (X : AlgebraicGeometry.Scheme), X.nilradical = ⊥.radical
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RocSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Roc α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Roc α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1