mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Control.Except
liftExcept : {ε : Type u_1} → {m : Type u_2 → Type u_3} → {α : Type u_2} → [MonadExceptOf ε m] → [Pure m] → Except ε α → m α
-- Mathlib.Algebra.Module.Equiv.Defs
/-- The linear map underlying a linear equivalence.  -/
LinearEquiv.toLinearMap : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_16} →
                  {M₂ : Type u_17} →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] → [inst_7 : Module S M₂] → (M ≃ₛₗ[σ] M₂) → M →ₛₗ[σ] M₂
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The free topological module over a topological space as a functor.
This is left adjoint to the forgetful functor.  -/
TopModuleCat.free : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → CategoryTheory.Functor TopCat (TopModuleCat R)
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- If `f` is a morphism of `Arrow V`, this is a "candidate cokernel" of `f`, i.e. an object
in `Arrow V` whose image in `RightFreyd V` will be a cokernel of the image of `f`.  -/
CategoryTheory.Preadditive.RightFreyd.Candidate.cokernel : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      [CategoryTheory.Limits.HasBinaryBiproducts V] → {u v : CategoryTheory.Arrow V} → (u ⟶ v) → CategoryTheory.Arrow V
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_comp_heq_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) f ≍ g ↔ f ≍ g
-- Mathlib.RingTheory.Localization.Basic
/-- Another version of `IsLocalization.map_injective_of_injective` that is more general for the choice
of the localization submonoid but requires it does not contain zero.
 -/
IsLocalization.map_injective_of_injective' : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] {f : R →+* S}
  {Rₘ : Type u_3} [inst_2 : CommRing Rₘ] [inst_3 : Algebra R Rₘ] [inst_4 : IsLocalization M Rₘ] (Sₘ : Type u_4)
  {N : Submonoid S} [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ] [inst_7 : IsLocalization N Sₘ]
  (hf : M ≤ Submonoid.comap f N),
  0 ∉ N → ∀ [IsDomain S], Function.Injective ⇑f → Function.Injective ⇑(IsLocalization.map Sₘ f hf)
-- Mathlib.CategoryTheory.Pi.Basic
/-- The natural isomorphism comparing between
pulling back along two successive functions, and
pulling back along their composition
 -/
CategoryTheory.Pi.comapComp : {I : Type w₀} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₁} →
        {K : Type w₂} →
          (f : K → J) →
            (g : J → I) →
              (CategoryTheory.Pi.comap C g).comp (CategoryTheory.Pi.comap (C ∘ g) f) ≅ CategoryTheory.Pi.comap C (g ∘ f)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.coe_aeval_eq_eval : ∀ {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring S₁] (f : σ → S₁), ↑(MvPolynomial.aeval f) = MvPolynomial.eval f
-- Mathlib.Order.Ideal
Order.Ideal.mem_sup : ∀ {P : Type u_1} [inst : SemilatticeSup P] [inst_1 : IsCodirectedOrder P] {x : P} {I J : Order.Ideal P},
  x ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of `fderivWithin_const_smul_field`.

---

Special case of `fderivWithin_const_smul_of_invertible` over a division semiring: any constant
is allowed.

TODO: This would work for scalars in a `GroupWithZero` if we had a `DistribMulActionWithZero`
typeclass.  -/
fderivWithin_const_smul_of_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {R : Type u_4} [inst_5 : DivisionSemiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F] (c : R),
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x
-- Mathlib.RingTheory.Conductor
mem_coeSubmodule_conductor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {L : Type u_3}
  [inst_3 : CommRing L] [inst_4 : Algebra S L] [inst_5 : Algebra R L] [IsScalarTower R S L] [FaithfulSMul S L] {x : S}
  {y : L}, y ∈ IsLocalization.coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ R[(algebraMap S L) x]
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜}, iteratedDerivWithin 1 f s = derivWithin f s
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Collect the pattern (i.e., de Bruijn) variables in the given pattern.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collectPatternBVars : Lean.Expr → List ℕ
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_a_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a ≠ 0 → P.toPoly.leadingCoeff = P.a
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.mem_carrier : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  (L' : LieRinehartSubalgebra A L) {x : L}, x ∈ L'.carrier ↔ x ∈ ↑L'
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], ∅.max? = none
-- Aesop.Search.Expansion.Norm
Aesop.NormM.State.mk.injEq : ∀ (forwardState : Aesop.ForwardState) (forwardRuleMatches : Aesop.ForwardRuleMatches)
  (forwardState_1 : Aesop.ForwardState) (forwardRuleMatches_1 : Aesop.ForwardRuleMatches),
  ({ forwardState := forwardState, forwardRuleMatches := forwardRuleMatches } =
      { forwardState := forwardState_1, forwardRuleMatches := forwardRuleMatches_1 }) =
    (forwardState = forwardState_1 ∧ forwardRuleMatches = forwardRuleMatches_1)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.B.eq_1 : ∀ (n : ℕ),
  CartanMatrix.B n =
    Matrix.of fun i j =>
      if i = j then 2 else if ↑i + 1 = ↑j then if ↑j = n - 1 then -2 else -1 else if ↑j + 1 = ↑i then -1 else 0
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ShiftTarget.distance : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {w : ℕ} → aig.ShiftTarget w → ℕ
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry from a metric space is a uniform inducing map  -/
Isometry.isUniformInducing : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → IsUniformInducing f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- The right whiskering in the bicategory `Adj B`.  -/
CategoryTheory.Bicategory.Adj.Bicategory.whiskerRight : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : CategoryTheory.Bicategory.Adj B} →
      {α α' : a ⟶ b} →
        (α ⟶ α') → (β : b ⟶ c) → CategoryTheory.CategoryStruct.comp α β ⟶ CategoryTheory.CategoryStruct.comp α' β
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.PrepareRenameParams : Type
-- Mathlib.Tactic.NormNum.Ordinal
/-- The `norm_num` extension for strict inequality on ordinals.  -/
Mathlib.Meta.NormNum.evalOrdinalLT : Mathlib.Meta.NormNum.NormNumExt
-- Lean.Class
Lean.ClassState.mk : Lean.SMap Lean.Name (Array ℕ) → Lean.SMap Lean.Name (Array ℕ) → Lean.ClassState
-- Mathlib.Order.Sublattice
/-- The inf of sublattices is their intersection.  -/
Sublattice.instInfSet : {α : Type u_2} → [inst : Lattice α] → InfSet (Sublattice α)
-- Init.Data.List.Basic
List.unzip_nil : ∀ {α : Type u} {β : Type v}, [].unzip = ([], [])
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkAppS₁₁ : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] →
      Lean.Expr →
        Lean.Expr →
          Lean.Expr →
            Lean.Expr →
              Lean.Expr →
                Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- the underlying topological space of `Spec`  -/
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.«termSpec.T_» : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Associated
Associated.neg_right_iff : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : HasDistribNeg M] {a b : M}, Associated a (-b) ↔ Associated a b
-- Mathlib.RingTheory.Localization.Basic
Localization.mapPiEvalRingHom_bijective : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → CommSemiring (R i)] {i : ι} (S : Submonoid (R i)),
  Function.Bijective ⇑(Localization.mapPiEvalRingHom S)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorInclusion_top_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C}, CategoryTheory.IsIso ⊤.functorInclusion
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.comap_incl_eq_top : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I I₂ : LieIdeal R L},
  LieIdeal.comap I.incl I₂ = ⊤ ↔ I ≤ I₂
-- Mathlib.Order.Hom.Bounded
BotHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bot α] [inst_1 : Bot β] [inst_2 : Bot γ] {g₁ g₂ : BotHom β γ}
  {f : BotHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- For a functor `G : C ⥤ D`, and an object `U : D`, `Sieve.coverByImage G U` is the sieve of `U`
consisting of those arrows that factor through images of `G`.
 -/
CategoryTheory.Sieve.coverByImage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → (U : D) → CategoryTheory.Sieve U
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- `le_of_add_le_add_left` is normally applicable to ordered cancellative monoids,
but it holds for measures with the additional assumption that μ is finite.  -/
MeasureTheory.Measure.le_of_add_le_add_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  μ + ν₁ ≤ μ + ν₂ → ν₁ ≤ ν₂
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {G H : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (θ : G ⟶ H) {a b : B} {a' : CategoryTheory.Cat} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h) (X : ↑a'),
  CategoryTheory.CategoryStruct.comp ((θ.app b).toFunctor.map ((G.map₂ β).toNatTrans.app (f.toFunctor.obj X)))
      ((θ.naturality h).hom.toNatTrans.app (f.toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.comp ((θ.naturality g).hom.toNatTrans.app (f.toFunctor.obj X))
      ((H.map₂ β).toNatTrans.app ((θ.app a).toFunctor.obj (f.toFunctor.obj X)))
-- Mathlib.Algebra.Field.Subfield.Defs
/-- The embedding from a subfield of the field `K` to `K`.  -/
Subfield.subtype : {K : Type u} → [inst : DivisionRing K] → (s : Subfield K) → ↥s →+* K
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.coe_symm_opMulEquiv : ∀ {M : Type u_1} [inst : CommMonoid M], ⇑MulOpposite.opMulEquiv.symm = MulOpposite.unop
-- Lean.PrettyPrinter.Basic
Lean.PrettyPrinter.runForNodeKind : {α : Type} → Lean.KeyedDeclsAttribute α → Lean.SyntaxNodeKind → (Lean.ParserDescr → Lean.CoreM α) → Lean.CoreM α
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_iSup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F},
  Function.Surjective ⇑f → ∀ (S : ι → AddSubmonoid N), AddSubmonoid.map f (⨆ i, AddSubmonoid.comap f (S i)) = iSup S
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_one_comp_σ₂_one_assoc : ∀ {n : ℕ} (hn : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_one._auto_1)
  (hn' : autoParam ({ len := n + 1 + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_one._auto_3)
  {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := n + 1 }, property := hn } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.δ₂ 1 hn hn')
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.σ₂ 1 hn' hn) h) =
    h
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
IsIntegralClosure.mk'.eq_1 : ∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B] [inst_5 : IsIntegralClosure A R B] (x : B) (hx : IsIntegral R x),
  IsIntegralClosure.mk' A x hx = Classical.choose ⋯
-- Mathlib.Probability.Density
/-- **The Law of the Unconscious Statistician** for nonnegative random variables.  -/
MeasureTheory.pdf.lintegral_pdf_mul : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {X : Ω → E} [MeasureTheory.HasPDF X ℙ μ] {f : E → ENNReal},
  AEMeasurable f μ → ∫⁻ (x : E), MeasureTheory.pdf X ℙ μ x * f x ∂μ = ∫⁻ (x : Ω), f (X x) ∂ℙ
-- Mathlib.Topology.PartitionOfUnity
/-- A partition of unity `f i` is subordinate to a family of sets `U i` indexed by the same type if
for each `i` the closure of the support of `f i` is a subset of `U i`.  -/
PartitionOfUnity.IsSubordinate : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → PartitionOfUnity ι X s → (ι → Set X) → Prop
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.mem_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {y : N}, y ∈ f.range ↔ ∃ x, f x = y
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.eq_empty_or_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} [WellFoundedGT α], IsLowerSet s → s = ∅ ∨ ∃ a, s = Set.Iic a
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_mul : ∀ {α : Type u_1} (xs ys : FreeMonoid α), FreeMonoid.toList (xs * ys) = FreeMonoid.toList xs ++ FreeMonoid.toList ys
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.instInhabitedHomOplaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → {F G : CategoryTheory.OplaxFunctor B C} → {η : F ⟶ G} → Inhabited (η ⟶ η)
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.mem_lifts_of_surjective : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S},
  Function.Surjective ⇑f → ∀ (p : Polynomial S), p ∈ Polynomial.lifts f
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `N` is a normal subgroup of `G` and `IsGaloisGroup N B C`, then `G` acts on `B` as a
`MulSemiringAction`, via the action defined in `smulOfNormal`.  -/
IsGaloisGroup.mulSemiringActionOfNormal : (G : Type u_1) →
  [inst : Group G] →
    (B : Type u_3) →
      (C : Type u_4) →
        [inst_1 : Semiring C] →
          [inst_2 : MulSemiringAction G C] →
            (N : Subgroup G) →
              [inst_3 : CommSemiring B] →
                [inst_4 : Algebra B C] →
                  [FaithfulSMul B C] → [IsGaloisGroup (↥N) B C] → [N.Normal] → MulSemiringAction G B
-- Mathlib.Topology.Metrizable.Basic
/-- A topological space is *pseudometrizable* if there exists a pseudometric space structure
compatible with the topology. To minimize imports, we implement this class in terms of the
existence of a countably generated uniformity inducing the topology, which is mathematically
equivalent.
To endow such a space with a compatible uniformity, use
`letI : UniformSpace X := TopologicalSpace.pseudoMetrizableSpaceUniformity X`.
To endow such a space with a compatible distance, use
`letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X`.  -/
TopologicalSpace.PseudoMetrizableSpace : (X : Type u_5) → [t : TopologicalSpace X] → Prop
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_nonneg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  0 ≤ s.exradius signs
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_isBasis' : ∀ {α : Type u_1} {M : Matroid α} {I J X C : Set α},
  M.IsBasis' I X → M.IsBasis' J C → M.Indep (I \ C ∪ J) → (M.contract C).IsBasis' (I \ C) (X \ C)
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.NullSingletonClass.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  (∀ (x : α), μ {x} = 0) → MeasureTheory.NullSingletonClass μ
-- Lean.Elab.Tactic.Ext
/-- Applies extensionality theorems recursively, using `pats` to introduce variables in the result.
Runs continuation `k` on each subgoal.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.withExtN : {m : Type → Type u_1} →
  [Monad m] →
    [MonadLiftT Lean.Elab.TermElabM m] →
      [MonadExcept Lean.Exception m] →
        Lean.MVarId →
          List (Lean.TSyntax `rcasesPat) →
            (Lean.MVarId → List (Lean.TSyntax `rcasesPat) → m ℕ) → optParam ℕ 100 → optParam Bool true → m ℕ
-- Lean.Elab.PreDefinition.FixedParams
/-- If `xs` are arguments to the `funIdx`'s function, pick only the varying ones.
Unlike `pickFixed`, this function can handle over- or under-application.
 -/
Lean.Elab.FixedParamPerm.pickVarying : {α : Type} → Lean.Elab.FixedParamPerm → Array α → Array α
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.X_add_C_ne_zero : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] (r : R), Polynomial.X + Polynomial.C r ≠ 0
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- In any abelian category with enough projectives,
`ProjectiveResolution.of Z` constructs a projective resolution of the object `Z`.
 -/
CategoryTheory.ProjectiveResolution.of : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [CategoryTheory.EnoughProjectives C] → (Z : C) → CategoryTheory.ProjectiveResolution Z
-- Mathlib.Analysis.Normed.Operator.Basic
/-- Continuous linear maps themselves form a seminormed space with respect to the operator norm.  -/
ContinuousLinearMap.toSeminormedAddCommGroup : {𝕜 : Type u_1} →
  {𝕜₂ : Type u_2} →
    {E : Type u_4} →
      {F : Type u_5} →
        [inst : SeminormedAddCommGroup E] →
          [inst_1 : SeminormedAddCommGroup F] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NontriviallyNormedField 𝕜₂] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜₂ F] →
                    {σ₁₂ : 𝕜 →+* 𝕜₂} → [RingHomIsometric σ₁₂] → SeminormedAddCommGroup (E →SL[σ₁₂] F)
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- The linear equivalence ` ⋀[R]^0 M ≃ₗ[R] R`.  -/
exteriorPower.zeroEquiv : (R : Type u) →
  [inst : CommRing R] → (M : Type u_1) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ↥(⋀[R]^0 M) ≃ₗ[R] R
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.ignoreTags.sizeOf_spec : sizeOf Lean.Widget.EmbedFmt.ignoreTags✝ = 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.code.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {code code_1 : Lean.Compiler.LCNF.Code pu},
  Lean.Compiler.LCNF.DeclValue.code code = Lean.Compiler.LCNF.DeclValue.code code_1 → code = code_1
-- Init.Data.UInt.Lemmas
UInt8.toNat_lt_usizeSize : ∀ (n : UInt8), n.toNat < USize.size
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The functor part of the equivalence `LightProfinite ≌ LightDiagram`  -/
lightProfiniteToLightDiagram : CategoryTheory.Functor LightProfinite LightDiagram
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to an `Hour.Offset`.
 -/
Std.Time.Second.Offset.toHours : Std.Time.Second.Offset → Std.Time.Hour.Offset
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) UInt16.toUInt8_ofNatClamp_of_le._proof_1
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_comp : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5} {E'' : ι → Type u_6}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  [inst_6 : (i : ι) → SeminormedAddCommGroup (E'' i)] [inst_7 : (i : ι) → NormedSpace 𝕜 (E'' i)]
  (g : (i : ι) → E' i →L[𝕜] E'' i) (f : (i : ι) → E i →L[𝕜] E' i),
  (PiTensorProduct.mapL fun i => g i ∘SL f i) = PiTensorProduct.mapL g ∘SL PiTensorProduct.mapL f
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.topIso_hom : ∀ (X : AlgebraicGeometry.Scheme), X.topIso.hom = ⊤.ι
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.cyclesIsoH.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁),
  X.cyclesIsoH f n₀ n₁ hn₁ =
    (X.cyclesIso (CategoryTheory.CategoryStruct.id i₀) f (CategoryTheory.CategoryStruct.id i₁) (n₀ - 1) n₀ n₁ ⋯
          hn₁).symm ≪≫
      (X.homologyDataIdId f (n₀ - 1) n₀ n₁ ⋯ ⋯).left.cyclesIso
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.toHomeomorph_uniformEquiv : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → UniformSpace (β i)],
  (PiLp.uniformEquiv p β).toHomeomorph = PiLp.homeomorph p β
-- Aesop.Rule.Name
Aesop.instHashableDisplayRuleName.hash : Aesop.DisplayRuleName → UInt64
-- Mathlib.Analysis.SumIntegralExpDecay
sum_Iic_pow_mul_exp_neg_le : ∀ {k M : ℕ} {c : ℝ}, 0 < c → ∑ i ≤ M, ↑i ^ k * Real.exp (-(c * ↑i)) ≤ Real.exp c * ↑k.factorial / c ^ (k + 1)
-- Mathlib.Algebra.Order.Star.Basic
IsSelfAdjoint.sq_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {a : R},
  IsSelfAdjoint a → 0 ≤ a ^ 2
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.dvd_of_dvd_mul_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [DecompositionMonoid α], IsRelPrime x y → x ∣ y * z → x ∣ z
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Extend `Set α → E →L[ℝ] F` to `(α →₁ₛ[μ] E) →L[ℝ] F`.  -/
MeasureTheory.L1.SimpleFunc.setToL1SCLM : (α : Type u_1) →
  (E : Type u_2) →
    {F : Type u_3} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {m : MeasurableSpace α} →
                (μ : MeasureTheory.Measure α) →
                  {T : Set α → E →L[ℝ] F} →
                    {C : ℝ} → MeasureTheory.DominatedFinMeasAdditive μ T C → ↥(α →₁ₛ[μ] E) →L[ℝ] F