mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.sum_measure_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  {μ : MeasureTheory.Measure α} (s : Finset β), ∑ y ∈ s, μ (⇑f ⁻¹' {y}) = μ (⇑f ⁻¹' ↑s)
-- Init.Data.UInt.Lemmas
USize.toFin_ofNatTruncate_of_le : ∀ {n : ℕ}, USize.size ≤ n → (USize.ofNatClamp n).toFin = ⟨USize.size - 1, USize.toFin_ofNatClamp_of_le._proof_1⟩
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.empty_vecMulVec : ∀ {α : Type u} {n' : Type uₙ} [inst : NonUnitalNonAssocSemiring α] (v : Fin 0 → α) (w : n' → α),
  Matrix.vecMulVec v w = Matrix.of ![]
-- Lean.Elab.Arg
Lean.Elab.Term.instInhabitedArg.default : Lean.Elab.Term.Arg
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The underlying lean expression of a 2-isomorphism.  -/
Mathlib.Tactic.BicategoryLike.StructuralAtom.e : Mathlib.Tactic.BicategoryLike.StructuralAtom → Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF], W.c₄ = 16 * W.a₂ ^ 2
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_eq_of_associated : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, Associated a b → UniqueFactorizationMonoid.radical a = UniqueFactorizationMonoid.radical b
-- Mathlib.Logic.Relation
/-- To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,
it suffices to show it holds when `x ≠ y`.  -/
Std.Refl.rel_of_ne_imp : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {x y : α}, (x ≠ y → r x y) → r x y
-- Mathlib.Algebra.BigOperators.Associated
Finset.prod_primes_dvd : ∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [IsCancelMulZero M₀] [Subsingleton M₀ˣ] {s : Finset M₀} (n : M₀),
  (∀ a ∈ s, Prime a) → (∀ a ∈ s, a ∣ n) → ∏ p ∈ s, p ∣ n
-- Mathlib.CategoryTheory.Subfunctor.Finite
/-- Objects on which a choice of generating sections of a finitely generated subpresheaf
are defined.  -/
CategoryTheory.Subfunctor.IsFinite.X : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {G : CategoryTheory.Subfunctor F} → [hG : G.IsFinite] → CategoryTheory.Subfunctor.IsFinite.Index G → Cᵒᵖ
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coordChangeL_symm_apply : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet),
  ⇑(Bundle.Trivialization.coordChangeL R e e' b).symm =
    ⇑((Bundle.Trivialization.linearEquivAt R e' b ⋯).symm ≪≫ₗ Bundle.Trivialization.linearEquivAt R e b ⋯)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFractionRel.refl : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (z : W.LeftFraction X Y), CategoryTheory.MorphismProperty.LeftFractionRel z z
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Entries for the `apply at` discrimination tree.  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Entries.appAt : Mathlib.Tactic.ClickSuggestions.Entries✝ →
  Array
    (Lean.Meta.RefinedDiscrTree.Key ×
      Lean.Meta.RefinedDiscrTree.LazyEntry × Mathlib.Tactic.ClickSuggestions.ApplyAtLemma)
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.order_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R),
  ((MvPowerSeries.expand p hp) φ).order = p • φ.order
-- Lean.Meta.Sym.InstantiateMVarsS
/-- Head-only variant of `instantiateMVarsS`: instantiates and reshares only when the head of `e` is a
metavariable, otherwise returns `e` unchanged.
 -/
Lean.Meta.Sym.instantiateMVarsIfMVarAppS : Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.polynomial.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R),
  W'.polynomial =
    MvPolynomial.X 1 ^ 2 + MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 * MvPolynomial.X 2 +
        MvPolynomial.C W'.a₃ * MvPolynomial.X 1 * MvPolynomial.X 2 ^ 3 -
      (MvPolynomial.X 0 ^ 3 + MvPolynomial.C W'.a₂ * MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 ^ 2 +
          MvPolynomial.C W'.a₄ * MvPolynomial.X 0 * MvPolynomial.X 2 ^ 4 +
        MvPolynomial.C W'.a₆ * MvPolynomial.X 2 ^ 6)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearMap_symm : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (φ : ρ.Equiv σ), (↑φ.symm).toLinearMap = ↑φ.toLinearEquiv.symm
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_get?_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  (t.get? a).isSome = true ↔ a ∈ t
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.instSeparableSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.SeparableSpace α],
  TopologicalSpace.SeparableSpace (TopologicalSpace.Compacts α)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeOp_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Functor.mapCoconeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
-- Mathlib.Data.Finsupp.Lex
/-- `Finsupp.Lex r s` is the lexicographic relation on `α →₀ N`, where `α` is ordered by `r`,
and `N` is ordered by `s`.

The type synonym `Lex (α →₀ N)` has an order given by `Finsupp.Lex (· < ·) (· < ·)`.
 -/
Finsupp.Lex : {α : Type u_1} → {N : Type u_2} → [inst : Zero N] → (α → α → Prop) → (N → N → Prop) → (α →₀ N) → (α →₀ N) → Prop
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instDistribSMulOfSMulCommClass : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {X : Type u_4} →
        {Y : Type u_5} →
          {σ : M → N} →
            [inst : AddZeroClass Y] →
              [inst_1 : SMul M X] →
                [inst_2 : DistribSMul N Y] →
                  [inst_3 : DistribSMul R Y] → [SMulCommClass N R Y] → DistribSMul R (X →ₑ[σ] Y)
-- Mathlib.RingTheory.AdicCompletion.Topology
WithIdeal.uniformEquiv.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : WithIdeal R] {S : Type u_2} [inst_2 : CommRing S] [inst_3 : WithIdeal S]
  (e e_1 : R ≃+* S) (e_e : e = e_1) (h : Ideal.map e.toRingHom WithIdeal.i = WithIdeal.i),
  WithIdeal.uniformEquiv e h = WithIdeal.uniformEquiv e_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
/-- Finite form of Euler's sine product, with remainder term expressed as a ratio of cosine
integrals.  -/
EulerSine.sin_pi_mul_eq : ∀ (z : ℂ) (n : ℕ),
  Complex.sin (↑Real.pi * z) =
    ((↑Real.pi * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
        ∫ (x : ℝ) in 0..Real.pi / 2, Complex.cos (2 * z * ↑x) * ↑(Real.cos x) ^ (2 * n)) /
      ↑(∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ (2 * n))
-- Mathlib.MeasureTheory.Function.Floor
Measurable.floor : ∀ {α : Type u_1} {R : Type u_2} [inst : MeasurableSpace α] [inst_1 : Ring R] [inst_2 : LinearOrder R]
  [inst_3 : FloorRing R] [inst_4 : TopologicalSpace R] [OrderTopology R] [inst_6 : MeasurableSpace R]
  [OpensMeasurableSpace R] {f : α → R}, Measurable f → Measurable fun x => ⌊f x⌋
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.RotateRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} (input input_1 : aig.RefVec w),
  input = input_1 →
    ∀ (distance distance_1 : ℕ),
      distance = distance_1 →
        ∀ (curr : ℕ) (hcurr : curr ≤ w) (s s_1 : aig.RefVec curr),
          s = s_1 →
            Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go input distance curr hcurr s =
              Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go input_1 distance_1 curr hcurr s_1
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_fp : ∀ {f : Ordinal.{u} → Ordinal.{u}}, Order.IsNormal f → ∀ (a : Ordinal.{u}), f (Ordinal.nfp f a) = Ordinal.nfp f a
-- Mathlib.Algebra.Ring.BooleanRing
/-- The "identity" equivalence between `α` and `AsBoolRing α`.  -/
ofBoolRing : {α : Type u_1} → AsBoolRing α ≃ α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roc_eq_zero : ∀ {m n i : ℕ}, n ≤ i + m → (m<...=n).toList[i]! = 0
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.isColimit_sigma : ∀ {C : Type u} (F : C → Type v), CategoryTheory.Functor.CoconeTypes.IsColimit (CategoryTheory.Limits.CofanTypes.sigma F)
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.IterM.forIn_filterMapWithPostcondition : ∀ {α β β₂ γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} {Pred EPred : Type w}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o]
  [inst_5 : Std.Internal.Do.Assertion Pred] [inst_6 : Std.Internal.Do.Assertion EPred]
  [inst_7 : Std.Internal.Do.WPMonad o Pred EPred] [inst_8 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_10 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_12 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_14 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Pred}
  {Q : γ → Pred} {eQ : EPred},
  ⦃ P ⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        match __do_lift with
          | some c => g c acc
          | none => pure (ForInStep.yield acc) ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ forIn (Std.IterM.filterMapWithPostcondition f it) init g ⦃ Q; eQ ⦄
-- Lean.Parser.Command
Lean.Parser.Command.genInjectiveTheorems.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- `HasKernels` represents the existence of kernels for every morphism.  -/
CategoryTheory.Limits.HasKernels : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_zero : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ},
  0 < δ → ∀ (E : Set α) {x : α}, x ∉ Metric.thickening δ E → thickenedIndicatorAux δ E x = 0
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_sum_of_disjoint : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {ι : Type u_3} (t : Finset ι) (φ : ι → MvPolynomial σ R)
  [inst_1 : DecidableEq σ],
  Pairwise (Function.onFun Disjoint fun i => (φ i).vars) → (∑ i ∈ t, φ i).vars = t.biUnion fun i => (φ i).vars
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.instRefl : ∀ {S : Type u_3} [inst : Add S], Std.Refl AddCommute
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.Presentation.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (generators : M.GeneratingSections)
  (relations : (CategoryTheory.Limits.kernel generators.π).GeneratingSections) (generators_1 : M.GeneratingSections)
  (relations_1 : (CategoryTheory.Limits.kernel generators_1.π).GeneratingSections),
  ({ generators := generators, relations := relations } = { generators := generators_1, relations := relations_1 }) =
    (generators = generators_1 ∧ relations ≍ relations_1)
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of November.
 -/
Std.Time.Month.Ordinal.november : Std.Time.Month.Ordinal
-- Lean.Meta.Basic
Lean.Meta.instBEqExprConfigCacheKey : BEq Lean.Meta.ExprConfigCacheKey
-- Init.Data.List.Sublist
List.singleton_prefix_cons_iff : ∀ {α : Type u_1} {a b : α} {l : List α}, [a] <+: b :: l ↔ a = b
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_id : ∀ {R : Type u} [inst : Monoid R] {A : Type v} [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : DistribMulAction R A],
  ⇑(NonUnitalAlgHom.id R A) = id
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMapZero.toNNReal_smul : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] (r : NNReal) (f : ContinuousMapZero X ℝ),
  (r • f).toNNReal = r • f.toNNReal
-- Mathlib.CategoryTheory.CommSq
/-- `CommSq.mk'` is the dual of `CommSq.mk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.CommSq.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z},
  autoParam (CategoryTheory.CategoryStruct.comp g i = CategoryTheory.CategoryStruct.comp f h)
      CategoryTheory.CommSq.mk'._auto_1 →
    CategoryTheory.CommSq f g h i
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.setIntegral_sdiff`. -/
MeasureTheory.integral_diff : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  MeasurableSet t →
    MeasureTheory.IntegrableOn f s μ →
      t ⊆ s → ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ
-- Init.Data.List.Lemmas
List.any_eq : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, l.any p = decide (∃ x ∈ l, p x = true)
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.FreeCoequalizer.condition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X)
      (CategoryTheory.Monad.FreeCoequalizer.π X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.bottomMap X)
      (CategoryTheory.Monad.FreeCoequalizer.π X)
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.hId_iso_hom_app : ∀ {C₁ : Type u_1} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₃] (L : CategoryTheory.Functor C₁ C₃) (X : C₁),
  (CategoryTheory.CatCommSq.iso (CategoryTheory.Functor.id C₁) L L (CategoryTheory.Functor.id C₃)).hom.app X =
    CategoryTheory.CategoryStruct.id (L.obj X)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_comp : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S),
  (↑e.symm).comp ↑e = RingHom.id R
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- 1 is weighted homogeneous of degree 0.  -/
MvPolynomial.isWeightedHomogeneous_one : ∀ (R : Type u_1) {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M),
  MvPolynomial.IsWeightedHomogeneous w 1 0
-- Mathlib.CategoryTheory.Monad.Products
/-- The backward direction of the equivalence from algebras for the coproduct monad to the under
category.
 -/
CategoryTheory.underToAlgebra : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        CategoryTheory.Functor (CategoryTheory.Under X) (CategoryTheory.coprodMonad X).Algebra
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instHImp : {α : Type u_1} → [inst : TopologicalSpace α] → [CompactSpace α] → [T2Space α] → HImp (TopologicalSpace.CompactOpens α)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.instSmoothOfRelativeDimensionOfNatNatCompScheme : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z)
  [AlgebraicGeometry.SmoothOfRelativeDimension 0 f] [AlgebraicGeometry.SmoothOfRelativeDimension 0 g],
  AlgebraicGeometry.SmoothOfRelativeDimension 0 (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_obj_right : ∀ {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) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₂ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).inverse.obj X).right = X.right
-- Mathlib.Algebra.Lie.CartanSubalgebra
/-- A Cartan subalgebra is a nilpotent, self-normalizing subalgebra.

A _splitting_ Cartan subalgebra can be defined by mixing in `LieModule.IsTriangularizable R H L`.  -/
LieSubalgebra.IsCartanSubalgebra : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieSubalgebra R L → Prop
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
/-- If every `x` has a neighbourhood on which `F i` tends uniformly to `f`, then `F i` tends
locally uniformly to `f`. (Special case of `tendstoLocallyUniformlyOn_of_forall_exists_nhds`
where `s = univ`.)  -/
tendstoLocallyUniformly_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι}, (∀ (x : α), ∃ t ∈ nhds x, TendstoUniformlyOn F f p t) → TendstoLocallyUniformly F f p
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instOfRestrict : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopCat} (f : U ⟶ X.toTopCat)
  (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (X.ofRestrict hf)
-- Mathlib.Data.List.Basic
List.reverse_foldl : ∀ {α : Type u} {l : List α}, (List.foldl (fun t h => h :: t) [] l).reverse = l
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanQueryModuleParams.mk.sizeOf_spec : ∀ (sourceRequestID : Lean.JsonRpc.RequestID) (queries : Array Lean.Lsp.LeanModuleQuery),
  sizeOf { sourceRequestID := sourceRequestID, queries := queries } = 1 + sizeOf sourceRequestID + sizeOf queries
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpContext.triggerCharacter? : Lean.Lsp.SignatureHelpContext → Option String
-- Mathlib.RepresentationTheory.Coinvariants
/-- Given a normal subgroup `S ≤ G`, a `G`-representation `ρ` restricts to a `G`-representation on
the kernel of the quotient map to the coinvariants of `ρ|_S`.  -/
Representation.toCoinvariantsKer : {k : Type u_6} →
  {G : Type u_7} →
    {V : Type u_8} →
      [inst : CommRing k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              (ρ : Representation k G V) →
                (S : Subgroup G) →
                  [S.Normal] → Representation k G ↥(Representation.Coinvariants.ker (MonoidHom.comp ρ S.subtype))
-- Lean.Elab.Level
Lean.Elab.Level.mkFreshLevelMVar : Lean.Elab.Level.LevelElabM Lean.Level
-- Std.Data.HashMap.Lemmas
Std.HashMap.unitOfArray_eq_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} (a : Array α), Std.HashMap.unitOfArray a = Std.HashMap.unitOfList a.toList
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.instToJsonCallHierarchy.toJson : Lean.Lsp.Ipc.CallHierarchy → Lean.Json
-- Mathlib.NumberTheory.NumberField.Basic
/-- The canonical coercion from `𝓞 K` to `K`.  -/
NumberField.RingOfIntegers.val : {K : Type u_1} → [inst : Field K] → NumberField.RingOfIntegers K → K
-- Mathlib.Algebra.Homology.Homotopy
/-- The backward chain map  -/
HomotopyEquiv.inv : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} → {C D : HomologicalComplex V c} → HomotopyEquiv C D → (D ⟶ C)
-- Mathlib.Analysis.MellinTransform
MellinConvergent.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ),
  MellinConvergent f s = MeasureTheory.IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.State.mk : Lean.Meta.Simp.Cache →
  Lean.ExprSet →
    ℕ →
      List String →
        Mathlib.Meta.FunProp.GeneralTheorems → Mathlib.Meta.FunProp.GeneralTheorems → Mathlib.Meta.FunProp.State
-- Mathlib.LinearAlgebra.QuadraticForm.Dual
/-- The symmetric bilinear form on `Module.Dual R M × M` defined as
`B (f, x) (g, y) = f y + g x`.  -/
LinearMap.dualProd : (R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R (Module.Dual R M × M)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_update_zero : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] (m : ι → M) (i : ι),
  f (Function.update m i 0) = 0
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.SatelliteConfig.exists_normalized : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {N : ℕ} {τ : ℝ}
  (a : Besicovitch.SatelliteConfig E N τ),
  a.c (Fin.last N) = 0 →
    a.r (Fin.last N) = 1 →
      1 ≤ τ →
        ∀ (δ : ℝ),
          τ ≤ 1 + δ / 4 → δ ≤ 1 → ∃ c', (∀ (n : Fin N.succ), ‖c' n‖ ≤ 2) ∧ Pairwise fun i j => 1 - δ ≤ ‖c' i - c' j‖
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- The topology of bounded convergence on `E →L[𝕜] F`. This coincides with the topology induced by
the operator norm when `E` and `F` are normed spaces.  -/
ContinuousLinearMap.topologicalSpace : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_4} →
            {F : Type u_5} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module 𝕜₂ F] →
                      [inst_6 : TopologicalSpace E] →
                        [inst_7 : TopologicalSpace F] → [IsTopologicalAddGroup F] → TopologicalSpace (E →SL[σ] F)
-- Mathlib.Topology.Separation.Basic
closure_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x : X}, closure {x} = {x}
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.min_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : LinearOrder α], Finset.min 0 = 0
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instIsNonstrictStrictOrderLeLt : IsNonstrictStrictOrder ZFSet.{u_1} (fun x1 x2 => x1 ⊆ x2) fun x1 x2 => x1 ⊂ x2
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.constantCoeff_map : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S)
  (φ : MvPowerSeries σ R), MvPowerSeries.constantCoeff ((MvPowerSeries.map f) φ) = f (MvPowerSeries.constantCoeff φ)