mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The restriction of `f - μ • 1` to the `k`-fold generalized `μ`-eigenspace is nilpotent.  -/
Module.End.isNilpotent_restrict_sub_algebraMap : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (k : ℕ)
  (h :
    optParam (Set.MapsTo ⇑(f - (algebraMap R (Module.End R M)) μ) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k))
      ⋯),
  IsNilpotent (LinearMap.restrict (f - (algebraMap R (Module.End R M)) μ) h)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.symm_Rel : ∀ {ι : Type u_1} (c : ComplexShape ι) (i j : ι), c.symm.Rel i j = c.Rel j i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.leadingCoeff_eq_iff_of_forall_abs_le_one : ∀ {n : ℕ} {P : Polynomial ℝ},
  2 ≤ n →
    P.degree ≤ ↑n →
      (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) →
        (P.leadingCoeff = 2 ^ (n - 1) ↔ P = Polynomial.Chebyshev.T ℝ ↑n)
-- Lean.Meta.IndPredBelow
Lean.Meta.IndPredBelow.RecursionContext.mk.inj : ∀ {belows : Lean.FVarIdMap (Lean.Name × Lean.Expr)} {motives : Lean.FVarIdMap (ℕ × Lean.Expr)}
  {belows_1 : Lean.FVarIdMap (Lean.Name × Lean.Expr)} {motives_1 : Lean.FVarIdMap (ℕ × Lean.Expr)},
  { belows := belows, motives := motives } = { belows := belows_1, motives := motives_1 } →
    belows = belows_1 ∧ motives = motives_1
-- Lean.Meta.Tactic.Simp.Types
/-- Helper method for bootstrapping purposes.
It disables `arith` if support theorems have not been defined yet.
 -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.updateArith : Lean.Meta.Simp.Config → Lean.CoreM Lean.Meta.Simp.Config
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagAddMonoidHom_apply : ∀ (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [inst : AddZeroClass α] (M : Matrix (m × o) (n × o) α)
  (k : o), (Matrix.blockDiagAddMonoidHom m n o α) M k = M.blockDiag k
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_add : ∀ {α : Type u_1} {f g : α → ENNReal}, ∑' (a : α), (f a + g a) = ∑' (a : α), f a + ∑' (a : α), g a
-- Mathlib.Order.SuccPred.Limit
IsLUB.mem_of_not_isSuccPrelimit : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α] {s : Set α}, IsLUB s a → ¬Order.IsSuccPrelimit a → a ∈ s
-- Init.Data.BitVec.Basic
BitVec.instRepr : {n : ℕ} → Repr (BitVec n)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.isCorepresentable : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (e : F.CorepresentableBy X), F.IsCorepresentable
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.casesTypes : Lean.Meta.Grind.ExtensionState → Lean.Meta.Grind.CasesTypes
-- Mathlib.Order.SuccPred.Basic
OrderIso.map_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : PartialOrder β]
  [inst_3 : SuccOrder β] (f : α ≃o β) (a : α), f (Order.succ a) = Order.succ (f a)
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.zero_right : ∀ {M : Type u_2} [inst : AddZeroClass M] (a : M), AddCommute a 0
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.ext_iff : ∀ {x y : SimplexCategory}, x = y ↔ x.len = y.len
-- Mathlib.Topology.Order.Hom.Basic
/-- Reinterpret a `ContinuousOrderHom` as a `ContinuousMap`.  -/
ContinuousOrderHom.toContinuousMap : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] → [inst_2 : TopologicalSpace β] → [inst_3 : Preorder β] → (α →Co β) → C(α, β)
-- Mathlib.Algebra.Order.Group.MinMax
max_neg_zero : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] (a : α), max (-a) 0 = -a + max a 0
-- Std.Data.TreeSet.Raw.Basic
/-- Returns the `n`-th smallest element, or panics if `n` is at least `t.size`.  -/
Std.TreeSet.Raw.atIdx! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet.Raw α cmp → ℕ → α
-- Init.Data.Int.Linear
Int.Internal.Linear.ediv_emod : ∀ (x y : ℤ), -1 * x + y * (x / y) + x % y = 0
-- Mathlib.Algebra.Ring.Units
Units.add_divp : ∀ {α : Type u} [inst : Semiring α] (a b : α) (u : αˣ), a + b /ₚ u = (a * ↑u + b) /ₚ u
-- Mathlib.Analysis.Calculus.Deriv.Basic
UniqueDiffWithinAt.eq_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' f₁' : F} {x : 𝕜} (s : Set 𝕜),
  UniqueDiffWithinAt 𝕜 s x → HasDerivWithinAt f f' s x → HasDerivWithinAt f f₁' s x → f' = f₁'
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A],
  CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.preservesLimitIso A (F.comp (CategoryTheory.CategoryOfElements.π A))).inv)
      (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement' F)
-- Mathlib.Order.Filter.Finite
Set.Finite.eventuallyEq_iInter : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i =ᶠ[l] g i) → ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num_zero : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K], IsFractionRing.num A 0 = 0
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- The property of being a sum of squares is defined inductively by:
`0 : R` is a sum of squares and if `s : R` is a sum of squares,
then for all `a : R`, `a * a + s` is a sum of squares in `R`.
 -/
IsSumSq : {R : Type u_1} → [Mul R] → [Add R] → [Zero R] → R → Prop
-- Mathlib.CategoryTheory.GradedObject
/-- If `c : CofanMapObjFun X p j` is a colimit cofan, this is the induced
isomorphism `c.pt ≅ X.mapObj p j`.  -/
CategoryTheory.GradedObject.CofanMapObjFun.iso : {I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        {X : CategoryTheory.GradedObject I C} →
          {p : I → J} →
            {j : J} →
              [inst_1 : X.HasMap p] →
                {c : X.CofanMapObjFun p j} → CategoryTheory.Limits.IsColimit c → (c.pt ≅ X.mapObj p j)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- If `φ : W.LeftFraction X Y` and `L` is a functor which inverts `W`, this is the
induced morphism `L.obj X ⟶ L.obj Y`  -/
CategoryTheory.MorphismProperty.LeftFraction.map : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {W : CategoryTheory.MorphismProperty C} →
          {X Y : C} → W.LeftFraction X Y → (L : CategoryTheory.Functor C D) → W.IsInvertedBy L → (L.obj X ⟶ L.obj Y)
-- Mathlib.Data.Complex.Basic
Complex.I_zpow_eq_zpow_mod : ∀ (m : ℤ), Complex.I ^ m = Complex.I ^ (m % 4)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- If `F i → f` in `L1`, then `∫ᵛ x, F i x ∂[B; μ] → ∫ᵛ x, f x ∂[B; μ]`.  -/
MeasureTheory.VectorMeasure.tendsto_integral_of_L1' : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {ι : Type u_8} (f : X → E),
  MeasureTheory.AEStronglyMeasurable f μ.variation →
    ∀ {F_1 : ι → X → E} {l : Filter ι},
      (∀ᶠ (i : ι) in l, μ.Integrable (F_1 i)) →
        Filter.Tendsto (fun i => MeasureTheory.eLpNorm (F_1 i - f) 1 μ.variation) l (nhds 0) →
          Filter.Tendsto (fun i => ∫ᵛ (x : X), F_1 i x ∂[B; μ]) l (nhds ∫ᵛ (x : X), f x ∂[B; μ])
-- Mathlib.GroupTheory.SpecificGroups.Alternating
alternatingGroup.isMulCommutative_of_card_le_three : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Nat.card α ≤ 3 → IsMulCommutative ↥(alternatingGroup α)
-- Mathlib.Data.Fin.Basic
Fin.cast_eq_zero : ∀ {k l : ℕ} [inst : NeZero k] [inst_1 : NeZero l] (h : k = l) (x : Fin k), Fin.cast h x = 0 ↔ x = 0
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_eq_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t ∩ s = s ↔ s ⊆ t
-- Mathlib.Data.Set.Finite.Powerset
/-- There are finitely many subsets of a given finite set  -/
Set.Finite.finite_subsets : ∀ {α : Type u} {a : Set α}, a.Finite → {b | b ⊆ a}.Finite
-- Mathlib.Order.WithBot
/-- Auxiliary definition for the order on `WithBot`.  -/
WithBot.LE : {α : Type u_1} → [LE α] → WithBot α → WithBot α → Prop
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.id_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (M : Action V G),
  (Action.Hom.id M).hom = CategoryTheory.CategoryStruct.id M.V
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- The Riemann-Lebesgue lemma for functions on `ℝ`, formulated via
`Real.instFourierTransform.fourier`.  -/
Real.zero_at_infty_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E),
  Filter.Tendsto (FourierTransform.fourier f) (Filter.cocompact ℝ) (nhds 0)
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.lieQuotientLieRing : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (I : LieIdeal R L) → LieRing (L ⧸ I)
-- Mathlib.CategoryTheory.Abelian.Ext
ChainComplex.linearYonedaObj_d : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : CategoryTheory.Abelian C] {α : Type u_3}
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] (X : ChainComplex C α) (A : Type u_4) [inst_4 : Ring A]
  [inst_5 : CategoryTheory.Linear A C] (Y : C) (i j : α),
  (X.linearYonedaObj A Y).d i j = ModuleCat.ofHom (CategoryTheory.Linear.leftComp A Y (X.d j i))
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orImpR.sizeOf_spec : ∀ (p : Mathlib.Tactic.ITauto.Proof), sizeOf p.orImpR = 1 + sizeOf p
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.sum_cos : ∀ (n : ℕ) {a : ℝ},
  (∀ (k : ℤ), a ≠ ↑k * (2 * Real.pi)) →
    ∀ (b : ℝ),
      ∑ i ∈ Finset.range n, Real.cos (a * ↑i + b) =
        Real.sin (↑n * a / 2) * Real.cos ((↑n - 1) * a / 2 + b) / Real.sin (a / 2)
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_fn_integral_sub : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] {E' : Type u_5} [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace ℝ E']
  ⦃f g : β × γ → E⦄ (F : E → E'),
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable g ((κ.compProd η) a) →
      ∫ (x : β), F (∫ (y : γ), f (x, y) - g (x, y) ∂η (a, x)) ∂κ a =
        ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) - ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a
-- Mathlib.Topology.Bornology.Basic
/-- **Alias** of the forward direction of `Bornology.isBounded_compl_iff`. -/
Bornology.IsBounded.of_compl : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded sᶜ → Bornology.IsCobounded s
-- Mathlib.Algebra.GCDMonoid.Nat
/-- Maps an associate class of integers consisting of `-n, n` to `n : ℕ`  -/
associatesIntEquivNat : Associates ℤ ≃ ℕ
-- Init.Data.Vector.Lemmas
Vector.swapAt!_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n) {i : ℕ} {x : α},
  (Vector.mk xs h).swapAt! i x = ((xs.swapAt! i x).1, Vector.mk (xs.swapAt! i x).2 ⋯)
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.of.eq_1 : ∀ (M : Type u) [inst : AddSemigroup M], AddSemigrp.of M = { carrier := M, str := inst }
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.setOfPred_dep_eq : ∀ {α : Type u_1} (M : Matroid α), {D | M.Dep D} = {I | M.Indep I}ᶜ ∩ Set.Iic M.E
-- Aesop.RulePattern
/-- An expression of the form `λ y₀ ... yₖ, p` representing the
pattern.
 -/
Aesop.RulePattern.pattern : Aesop.RulePattern → Lean.Meta.AbstractMVarsResult
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.comp_mapAddGrp_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  (A : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε (F.comp G))
      ((F.comp G).map CategoryTheory.AddMonObj.zero)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (k : α), (t₁.erase k).Equiv (t₂.erase k)
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_eq_zero_of_order_zero : ∀ {G : Type u} [inst : Monoid G] {g : G}, orderOf g = 0 → Monoid.exponent G = 0
-- Mathlib.Algebra.Group.Basic
add_rotate' : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c : G), a + (b + c) = b + (c + a)
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrictComp_surjective : ∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F) (hq : q.natDegree ≠ 0),
  Function.Surjective ⇑(Polynomial.Gal.restrictComp p q hq)
-- Init.Data.Vector.Algebra
Vector.sub_eq_add_neg : ∀ {α : Type u_1} {n : ℕ} [inst : Sub α] [inst_1 : Add α] [inst_2 : Neg α],
  (∀ (x y : α), x - y = x + -y) → ∀ (xs ys : Vector α n), xs - ys = xs + -ys
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.desc_obj : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : (i : I) → CategoryTheory.Functor (C i) D) (X : (i : I) × C i),
  (CategoryTheory.Sigma.desc F).obj X = (F X.fst).obj X.snd
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trTape'_move_right : ∀ {Γ : Type u_1} {n : ℕ} {enc : Γ → List.Vector Bool n} [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (L R : Turing.ListBlank Γ),
  (Turing.Tape.move Turing.Dir.right)^[n] (Turing.TM1to1.trTape' enc0 L R) =
    Turing.TM1to1.trTape' enc0 (Turing.ListBlank.cons R.head L) R.tail
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_constantsToVars : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'}
  [inst_1 : (L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {t : (L.withConstants α).Term β}
  {v : β → M},
  FirstOrder.Language.Term.realize (Sum.elim (fun a => ↑(L.con a)) v) t.constantsToVars =
    FirstOrder.Language.Term.realize v t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.add_of_equiv : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P Q : Fin 3 → R},
  P ≈ Q → W'.add P Q = W'.dblXYZ P
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_ofInv_hom_id : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) (L.map s) =
    CategoryTheory.CategoryStruct.id (L.obj X)
-- Init.Core
Std.LawfulIdentity.toLawfulLeftIdentity : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} [self : Std.LawfulIdentity op o], Std.LawfulLeftIdentity op o
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovEDist_le_max_measure_univ : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] (μ ν : MeasureTheory.Measure Ω),
  MeasureTheory.levyProkhorovEDist μ ν ≤ max (μ Set.univ) (ν Set.univ)
-- Lean.Expr
/-- Uses `binderInfos?` to update the binder infos of the corresponding forall expressions.
 -/
Lean.Expr.updateForallBinderInfos : Lean.Expr → List (Option Lean.BinderInfo) → Lean.Expr
-- Mathlib.Data.Real.ConjExponents
/-- **Alias** of the reverse direction of `ENNReal.holderConjugate_coe_iff`. -/
NNReal.HolderConjugate.coe_ennreal : ∀ {p q : NNReal}, p.HolderConjugate q → (↑p).HolderConjugate ↑q
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit : {α : Type u} →
  {ρ : Type w} →
    [ForIn Id ρ α] →
      [inst : BEq α] →
        [inst_1 : Hashable α] →
          (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) →
            ρ →
              { m' //
                ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => Unit) → Prop),
                  (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {a : α} {b : Unit},
                      P m'' → P (m''.insertIfNew a b)) →
                    P m → P m' }
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousOn_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {z : β},
  LowerSemicontinuousOn (fun _x => z) s
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.contains'.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.eventually : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : Filter α},
  μ.FiniteAtFilter f → ∀ᶠ (s : Set α) in f.smallSets, μ s < ⊤
-- Std.Async.System
Std.Async.System.instOrdGroupId : Ord Std.Async.System.GroupId
-- Mathlib.Condensed.TopCatAdjunction
/-- The functor from topological spaces to condensed sets restricted to compactly generated spaces.
 -/
CondensedSet.compactlyGeneratedToCondensedSet : CategoryTheory.Functor CompactlyGenerated CondensedSet
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.rightOp_map_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ D} {X Y : C} (f : X ⟶ Y), (F.rightOp.map f).unop = F.map f.op
-- Init.Data.String.Defs
String.Slice.Pos.mk.inj : ∀ {s : String.Slice} {offset : String.Pos.Raw} {isValidForSlice : String.Pos.Raw.IsValidForSlice s offset}
  {offset_1 : String.Pos.Raw} {isValidForSlice_1 : String.Pos.Raw.IsValidForSlice s offset_1},
  { offset := offset, isValidForSlice := isValidForSlice } =
      { offset := offset_1, isValidForSlice := isValidForSlice_1 } →
    offset = offset_1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.hasBasis_uniformity_of_basis_aux₂ : ∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)),
  DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
    ∀ {p : ι → Prop} {s : ι → Set (β × β)},
      (uniformity β).HasBasis p s →
        DirectedOn ((fun s => UniformSpace.comap s.domRestrict (UniformFun.uniformSpace (↑s) β)) ⁻¹'o GE.ge) 𝔖
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.center_eq_infi' : ∀ {G : Type u_1} [inst : AddGroup G] {s : Set G},
  AddSubgroup.closure s = ⊤ → AddSubgroup.center G = ⨅ g, AddSubgroup.centralizer {↑g}
-- Mathlib.Data.Finset.Insert
Finset.Nontrivial.not_subset_singleton : ∀ {α : Type u_1} {s : Finset α} {a : α}, s.Nontrivial → ¬s ⊆ {a}
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.eq_1 : ∀ (x : String) (x_1 x_2 : String.Pos.Raw),
  String.Pos.Raw.extract x x_1 x_2 =
    if x_1.byteIdx ≥ x_2.byteIdx then "" else String.ofList (String.Pos.Raw.extract.go₁ x.toList 0 x_1 x_2)
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d₀_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (self : CochainComplex.ConnectData K L),
  CategoryTheory.CategoryStruct.comp self.d₀ (L.d 0 1) = 0
-- Mathlib.Algebra.Group.Action.Prod
MulAction.prodOfSMulCommClass.eq_1 : ∀ (M : Type u_1) (N : Type u_2) (α : Type u_5) [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : MulAction M α]
  [inst_3 : MulAction N α] [inst_4 : SMulCommClass M N α],
  MulAction.prodOfSMulCommClass M N α = { smul := fun mn a => mn.1 • mn.2 • a, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.le_iff_mem : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] {x : A} {s : Subalgebra R A},
  IsClosed ↑s → (Algebra.elemental R x ≤ s ↔ x ∈ s)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.mk.inj : ∀ {imports : Array Lean.Import} {pos : String.Pos.Raw} {badModifier : Bool} {error? : Option String}
  {isModule isMeta isExported importAll : Bool} {imports_1 : Array Lean.Import} {pos_1 : String.Pos.Raw}
  {badModifier_1 : Bool} {error?_1 : Option String} {isModule_1 isMeta_1 isExported_1 importAll_1 : Bool},
  { imports := imports, pos := pos, badModifier := badModifier, error? := error?, isModule := isModule,
        isMeta := isMeta, isExported := isExported, importAll := importAll } =
      { imports := imports_1, pos := pos_1, badModifier := badModifier_1, error? := error?_1, isModule := isModule_1,
        isMeta := isMeta_1, isExported := isExported_1, importAll := importAll_1 } →
    imports = imports_1 ∧
      pos = pos_1 ∧
        badModifier = badModifier_1 ∧
          error? = error?_1 ∧
            isModule = isModule_1 ∧ isMeta = isMeta_1 ∧ isExported = isExported_1 ∧ importAll = importAll_1
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.precheckChoice : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_period : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddGroup α],
  Function.Periodic f c₁ → Function.Periodic f c₂ → Function.Periodic f (c₁ - c₂)
-- Mathlib.Tactic.ProdAssoc
/-- Make a `ProdTree` out of an `Expr`.  -/
Lean.Expr.mkProdTree : Lean.Expr → Lean.MetaM Lean.Expr.ProdTree
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.hasEval_iff : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] {a : S},
  PowerSeries.HasEval a ↔ MvPowerSeries.HasEval fun x => a
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.parallelComp_sum_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {ι : Type u_5} [inst : Countable ι]
  (κ : ProbabilityTheory.Kernel α β) (η : ι → ProbabilityTheory.Kernel γ δ)
  [∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (η i)],
  κ.parallelComp (ProbabilityTheory.Kernel.sum η) = ProbabilityTheory.Kernel.sum fun i => κ.parallelComp (η i)
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.Ctx.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Ring.Common.Cache (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα) →
        Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.RatCoeff
            (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα) →
          ℕ → Q(ℕ) → Q(Array «$α») → Array Q(«$α») → Mathlib.Tactic.Determinant.Ctx rα