mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.toSmoothPartitionOfUnity.congr_simp : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs fs_1 : SmoothBumpCovering ι I M s),
  fs = fs_1 →
    ∀ [inst_6 : T2Space M] [inst_7 : IsManifold I (↑⊤) M], fs.toSmoothPartitionOfUnity = fs_1.toSmoothPartitionOfUnity
-- Mathlib.LinearAlgebra.Span.Defs
/-- For every element in the span of a set, there exists a finite subset of the set
such that the element is contained in the span of the subset.  -/
Submodule.mem_span_finite_of_mem_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Set M}
  {x : M}, x ∈ Submodule.span R S → ∃ T, ↑T ⊆ S ∧ x ∈ Submodule.span R ↑T
-- Lean.Meta.Tactic.NormCast
/-- `addSquash decl` adds `decl` as a `squash` lemma to be used by `norm_cast`.  -/
Lean.Meta.NormCast.addSquash : Lean.Name → optParam Lean.AttributeKind Lean.AttributeKind.global → optParam ℕ 1000 → Lean.MetaM Unit
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- The actual `AddSubmonoid` obtained from an element of a
`AddSubmonoidClass`  -/
AddSubmonoid.ofClass : {S : Type u_3} →
  {M : Type u_4} → [inst : AddMonoid M] → [inst_1 : SetLike S M] → [AddSubmonoidClass S M] → S → AddSubmonoid M
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsGreatest.nnnorm_cfcₙ : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedSpace 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A]
  [inst_6 : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A),
  autoParam (ContinuousOn f (quasispectrum 𝕜 a)) IsGreatest.nnnorm_cfcₙ._auto_1 →
    autoParam (f 0 = 0) IsGreatest.nnnorm_cfcₙ._auto_3 →
      autoParam (p a) IsGreatest.nnnorm_cfcₙ._auto_5 → IsGreatest ((fun x => ‖f x‖₊) '' quasispectrum 𝕜 a) ‖cfcₙ f a‖₊
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_obj : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h))
              (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) =
          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h))
              (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom))
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁))
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_5)
  (a : B),
  (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).obj
      a =
    obj a
-- Mathlib.CategoryTheory.Category.Basic
/-- A morphism `f` is a monomorphism if it can be cancelled when postcomposed.  -/
CategoryTheory.Mono.right_cancellation : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y} [self : CategoryTheory.Mono f] {Z : C}
  (g h : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.comp h f → g = h
-- Lean.Meta.Constructions.SparseCasesOn
_private.Lean.Meta.Constructions.SparseCasesOn.0.Lean.Meta.SparseCasesOnKey.mk.injEq : ∀ (indName : Lean.Name) (ctors : Array Lean.Name) (isPrivate : Bool) (indName_1 : Lean.Name) (ctors_1 : Array Lean.Name)
  (isPrivate_1 : Bool),
  ({ indName := indName, ctors := ctors, isPrivate := isPrivate } =
      { indName := indName_1, ctors := ctors_1, isPrivate := isPrivate_1 }) =
    (indName = indName_1 ∧ ctors = ctors_1 ∧ isPrivate = isPrivate_1)
-- Mathlib.Analysis.CStarAlgebra.Spectrum
CStarAlgebra.le_nnnorm_of_mem_quasispectrum : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a : A} {x : NNReal}, x ∈ quasispectrum NNReal a → x ≤ ‖a‖₊
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumMap_onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language}
  {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂) (_n : ℕ) (a : L.Functions _n ⊕ L₁.Functions _n),
  (ϕ.sumMap ψ).onFunction a = Sum.map (fun f => ϕ.onFunction f) (fun f => ψ.onFunction f) a
-- Init.Tactics
/-- In induction alternative, which can have 1 or more cases on the left
and `_`, `?_`, or a tactic sequence after the `=>`.
 -/
Lean.Parser.Tactic.inductionAlt : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.σ_comp_πSummand_id_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {n : ℕ} (i : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (X.σ i)
      (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n + 1 }))) =
    0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_some_iff' : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {k k' : α},
  Std.Internal.List.getKey? k l = some k' ↔
    ∃ (h : Std.Internal.List.containsKey k l = true), Std.Internal.List.getKey k l h = k'
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.center.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  AddSubmonoid.center M = { carrier := Set.addCenter M, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Data.Finset.Max
/-- If there's more than 1 element, the min' is less than the max'. An alternate version of
`min'_lt_max'` which is sometimes more convenient.
 -/
Finset.min'_lt_max'_of_card : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (h₂ : 1 < s.card), s.min' ⋯ < s.max' ⋯
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerSemicontinuousWithinAt_iff_frequently`. -/
LowerSemicontinuousWithinAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α} {s : Set α},
  LowerSemicontinuousWithinAt f s x → ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≤ y) → f x ≤ y
-- Lean.Language.Basic
/-- Concrete snapshot value as `Dynamic`.  -/
Lean.Language.DynamicSnapshot.val : Lean.Language.DynamicSnapshot → Dynamic
-- Init.Data.Order.PackageFactories
Std.PartialOrderPackage.toPreorderPackage : {α : Type u} → [self : Std.PartialOrderPackage α] → Std.PreorderPackage α
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.iteratedFDerivComponent.eq_1 : ∀ {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] {α : Type u_1}
  [inst_6 : Fintype α] (f : ContinuousMultilinearMap 𝕜 E₁ G) {s : Set ι} (e : α ≃ ↑s)
  [inst_7 : DecidablePred fun x => x ∈ s],
  f.iteratedFDerivComponent e = (f.iteratedFDerivComponent e).mkContinuousMultilinear ‖f‖ ⋯
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.opcyclesFunctor.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i i_1 : ι),
  i = i_1 →
    ∀ [inst_2 : CategoryTheory.CategoryWithHomology C],
      HomologicalComplex.opcyclesFunctor C c i = HomologicalComplex.opcyclesFunctor C c i_1
-- Mathlib.RingTheory.Valuation.Basic
Valuation.mem_ltAddSubgroup_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {γ : Γ₀ˣ} {x : R}, x ∈ v.ltAddSubgroup γ ↔ v x < ↑γ
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- A variant of the Euler product for the Riemann zeta function.  -/
riemannZeta_eulerProduct_exp_log : ∀ {s : ℂ}, 1 < s.re → Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = riemannZeta s
-- Lean.Elab.App
/-- Remaining positional arguments to be elaborated.  -/
Lean.Elab.Term.ElabAppArgs.State.args : Lean.Elab.Term.ElabAppArgs.State → List Lean.Elab.Term.Arg
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_le_zero : ∀ {x : ℝ}, Real.arctan x ≤ 0 ↔ x ≤ 0
-- Mathlib.Computability.TuringMachine.Computable
/-- a TM2 machine has finitely many internal states.  -/
Turing.FinTM2.σFin : (self : Turing.FinTM2) → Fintype self.σ
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.neg_left : ∀ {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : TopologicalSpace N]
  {M : Type u_6} [inst_2 : AddCommGroup M] [inst_3 : TopologicalSpace M] [inst_4 : IsTopologicalAddGroup M]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v.MutuallySingular w → (-v).MutuallySingular w
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.hasGaussianLaw_eval : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ (t : T), ProbabilityTheory.HasGaussianLaw (X t) P
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_eq_some_maxKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {he : l.isEmpty = false},
  Std.Internal.List.maxKey? l = some (Std.Internal.List.maxKey l he)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₃ : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2),
  (X.ω₂.obj j).obj₃ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (j.map (CategoryTheory.homOfLE ⋯)))
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Std.Net.Addr
Std.Net.instInhabitedAddressFamily.default : Std.Net.AddressFamily
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- The rank `Matroid.eRk M X` of a set `X` is the `ℕ∞`-valued cardinality of each basis of `X`.
(See `Matroid.cRk` for a worse-behaved cardinal-valued version)  -/
Matroid.eRk : {α : Type u_1} → Matroid α → Set α → ℕ∞
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.map_surjective_of_comap_eq : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {P' : Algebra.Extension R S} {f : P.Hom P'},
  Function.Surjective ⇑f →
    Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker →
      Function.Surjective ⇑(Algebra.Extension.Cotangent.map f)
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_sq_eq_half_sub : ∀ (x : ℝ), Real.sin x ^ 2 = 1 / 2 - Real.cos (2 * x) / 2
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν] {s : Set α},
  MeasurableSet s → (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s
-- Init.Core
of_toBoolUsing_eq_true : ∀ {p : Prop} {d : Decidable p}, toBoolUsing d = true → p
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- (Noncomputably) bundle the data of a reflexive pair as a functor out of the walking reflexive
pair  -/
CategoryTheory.Limits.ofIsReflexivePair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : C} →
      (f g : A ⟶ B) →
        [CategoryTheory.IsReflexivePair f g] → CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C
-- Lean.Elab.Declaration
Lean.Elab.Command.elabAxiom : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.NumberTheory.Divisors
Nat.divisorsAntidiagonalList_one : Nat.divisorsAntidiagonalList 1 = [(1, 1)]
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instAdd : {R : Type u} → [inst : Semiring R] → Add (Polynomial R)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instCommRingCoeOfSubringClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → CommRing (R i)] →
              [∀ (i : ι), SubringClass (S i) (R i)] → CommRing (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_eq_mk : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R} (hx : v x ≠ 0), v.restrict x = ↑(MonoidWithZeroHom.valueGroup.mk (MonoidWithZeroHom.ofClass v) 1 x ⋯ hx)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_le_left : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α}
  [inst_2 : DecidablePred fun x => x ≤ a], a < b → {x ∈ Finset.Ico a b | x ≤ a} = {a}
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.map_aeval_eq_aeval_map : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_3} {T : Type u_4} {U : Type u_5} [inst_1 : Semiring S]
  [inst_2 : CommSemiring T] [inst_3 : Semiring U] [inst_4 : Algebra R S] [inst_5 : Algebra T U] {φ : R →+* T}
  {ψ : S →+* U},
  (algebraMap T U).comp φ = ψ.comp (algebraMap R S) →
    ∀ (p : Polynomial R) (a : S), ψ ((Polynomial.aeval a) p) = (Polynomial.aeval (ψ a)) (Polynomial.map φ p)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).hom
      (Y.ofRestrict ⋯) =
    f
-- Mathlib.NumberTheory.NumberField.Discriminant.Basic
NumberField.discr.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.discr K = NumberField.discr K
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- `C^n` scalar-valued functions act by left-multiplication on `C^n` functions.  -/
ContMDiffMap.instSMul' : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {V : Type u_10} →
                          [inst_6 : NormedAddCommGroup V] →
                            [inst_7 : NormedSpace 𝕜 V] →
                              SMul (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) N 𝕜 n)
                                (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.instIsIsoAppIncl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : SuccOrder J]
  [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J] {X Y : C} {f : X ⟶ Y}
  (h : (CategoryTheory.MorphismProperty.isomorphisms C).TransfiniteCompositionOfShape J f) (j : J),
  CategoryTheory.IsIso (h.incl.app j)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- Constructor for `Cocycle F G n`, taking as inputs `z : Cochain F G n`, an integer
`m : ℤ` such that `n + 1 = m`, and the relation `δ n m z = 0`.  -/
CochainComplex.HomComplex.Cocycle.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        {n : ℤ} →
          (z : CochainComplex.HomComplex.Cochain F G n) →
            (m : ℤ) → n + 1 = m → CochainComplex.HomComplex.δ n m z = 0 → CochainComplex.HomComplex.Cocycle F G n
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.disjoint_cylinder_of_longestPrefix_lt : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)},
  IsClosed s → ∀ {x : (n : ℕ) → E n}, x ∉ s → ∀ {n : ℕ}, PiNat.longestPrefix x s < n → Disjoint s (PiNat.cylinder x n)
-- Mathlib.Topology.Sheaves.SheafOfFunctions
/-- The sheaf of not-necessarily-continuous functions on `X` with values in a type `T`.
 -/
TopCat.sheafToType : (X : TopCat) → Type u_1 → TopCat.Sheaf (Type (max u_2 u_1)) X
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- All points have distance from the circumcenter equal to the
circumradius.  -/
Affine.Simplex.dist_circumcenter_eq_circumradius : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  dist (s.points i) s.circumcenter = s.circumradius
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.mk.sizeOf_spec : ∀ (A : Type uA) (B : A → Type uB), sizeOf { A := A, B := B } = 1 + sizeOf A
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- `parallelFamily f` is the diagram in `C` consisting of the given family of morphisms, each with
common domain and codomain.
 -/
CategoryTheory.Limits.parallelFamily : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} → (J → (X ⟶ Y)) → CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.Sheaf.mem_finestTopology_of_forall_isSheafFor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type w))} {X : C}
  {S : CategoryTheory.Sieve X},
  (∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) →
    S ∈ (CategoryTheory.Sheaf.finestTopology Ps) X
-- Init.Data.SInt.Lemmas
Int8.minValue_le : ∀ (a : Int8), Int8.minValue ≤ a
-- Init.Data.Nat.Basic
Nat.add_le_of_le_sub : ∀ {a b c : ℕ}, b ≤ c → a ≤ c - b → a + b ≤ c
-- Mathlib.Data.EReal.Operations
EReal.sub_bot : ∀ {x : EReal}, x ≠ ⊥ → x - ⊥ = ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.addY_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R},
  W'.Equation P → W'.addY P (W'.neg P) = -W'.dblZ P
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.comp_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {T : Type u_6} [inst_3 : CommRing T] [inst_4 : UniformSpace T]
  [inst_5 : T2Space T] [inst_6 : CompleteSpace T] [inst_7 : IsUniformAddGroup T] [inst_8 : IsTopologicalRing T]
  [inst_9 : IsLinearTopology T T] [inst_10 : Algebra R T] {ε : MvPowerSeries τ S →ₐ[R] T} [inst_11 : UniformSpace R]
  [inst_12 : DiscreteUniformity R] [inst_13 : UniformSpace S] [DiscreteUniformity S] (ha : MvPowerSeries.HasSubst a)
  (hε : Continuous ⇑ε), ⇑ε ∘ MvPowerSeries.subst a = ⇑(MvPowerSeries.aeval ⋯)
-- Lean.Parser.Term
Lean.Parser.Termination.decreasingBy.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Basic
/-- Register any local instance in `decls`  -/
Lean.Meta.withLocalInstances : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → List Lean.LocalDecl → n α → n α
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.disjoint_edgeFinset : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet],
  Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Line.mk.congr_simp : ∀ {α : Type u_5} {ι : Type u_6} (idxFun idxFun_1 : ι → Option α) (e_idxFun : idxFun = idxFun_1)
  (proper : ∃ i, idxFun i = none), { idxFun := idxFun, proper := proper } = { idxFun := idxFun_1, proper := ⋯ }
-- Init.Data.UInt.IntToBitVec
USize.lt_iff_toBitVec32_lt : ∀ {a b : USize} (h : System.Platform.numBits = 32), a < b ↔ a.toBitVec32 h < b.toBitVec32 h
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.counit_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : P.IsMonoidalStable] (c : CategoryTheory.WideSubcategory P)
  [inst_3 : CategoryTheory.ComonObj c.obj] [inst_4 : P.IsStableUnderComonoid c.obj],
  CategoryTheory.ComonObj.counit.hom = CategoryTheory.ComonObj.counit
-- Mathlib.Data.Analysis.Topology
instNonemptyRealizerOfFinite : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [Finite β] (F : Ctop.Realizer α) (f : β → Set α),
  Nonempty (LocallyFinite.Realizer F f)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smulFinset.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β],
  Finset.smulFinset = { smul := fun a => Finset.image fun x => a • x }
-- Mathlib.Data.List.Triplewise
List.Triplewise.brecOn : ∀ {α : Type u_1} {p : α → α → α → Prop} {motive : (a : List α) → List.Triplewise p a → Prop} {a : List α}
  (t : List.Triplewise p a),
  (∀ (a : List α) (t : List.Triplewise p a), List.Triplewise.below t → motive a t) → motive a t
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimit_obj_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  {H : CategoryTheory.Functor J (CategoryTheory.Functor K C)} [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  {k : K} {W : C} {f g : (CategoryTheory.Limits.colimit H).obj k ⟶ W},
  f = g ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι H j).app k) f =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.colimit.ι H j).app k) g