mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.Hom
/-- For a monoid `M` acting on a type `X`, the `M`-equivariant functions from `X` to itself
form a monoid under composition.  -/
MulActionHom.End.instMonoidId : {M : Type u_2} → {X : Type u_4} → [inst : SMul M X] → Monoid (X →ₑ[id] X)
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.chainLength_nsmul : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L)
  {x : L},
  x ∈ LieAlgebra.rootSpace H ⇑(LieModule.chainTop (⇑α) β) →
    LieAlgebra.IsKilling.chainLength α β • x = ⁅LieAlgebra.IsKilling.coroot α, x⁆
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccLimit_add_iff : ∀ {a b : Ordinal.{u_4}}, Order.IsSuccLimit (a + b) ↔ Order.IsSuccLimit b ∨ b = 0 ∧ Order.IsSuccLimit a
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.rIn_pos : ∀ {E : Type u_1} {c : E} (self : ContDiffBump c), 0 < self.rIn
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.contains_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.maxKey? = some km → t.contains km = true
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod_eq_one_iff_isFixedPt : ∀ {α : Type u_1} {f : α → α} {x : α}, Function.minimalPeriod f x = 1 ↔ Function.IsFixedPt f x
-- Mathlib.Algebra.Homology.Double
/-- Given a complex shape `c`, two indices `i₀` and `i₁` such that `c.Rel i₀ i₁`,
and `f : X₀ ⟶ X₁`, this is the homological complex which, if `i₀ ≠ i₁`, only
consists of the map `f` in degrees `i₀` and `i₁`, and zero everywhere else.  -/
HomologicalComplex.double : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasZeroObject C] →
        {X₀ X₁ : C} →
          (X₀ ⟶ X₁) → {ι : Type u_2} → {c : ComplexShape ι} → {i₀ i₁ : ι} → c.Rel i₀ i₁ → HomologicalComplex C c
-- Mathlib.RingTheory.HopfAlgebra.Convolution
LinearMap.comul_right_inv : ∀ {R : Type u_1} {C : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring C] [inst_2 : HopfAlgebra R C],
  WithConv.toConv CoalgebraStruct.comul * WithConv.toConv (CoalgebraStruct.comul ∘ₗ HopfAlgebraStruct.antipode R) = 1
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coe_mk : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (hμ : MeasureTheory.IsProbabilityMeasure μ),
  ↑⟨μ, hμ⟩ = μ
-- Lean.Elab.InfoTree.Types
/-- Context at the `CommandElabM/TermElabM` level. Created by `elabCommand` at the top level and then
nestedly when relevant fields are affected (e.g. just before discarding the `mctx` when exiting from
`TermElabM`).

Note that the term information collected during elaboration may contain metavariables, and their
assignments are stored at `mctx`.
 -/
Lean.Elab.CommandContextInfo : Type
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasis_dim : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K} (hf : f ≠ 0), (AdjoinRoot.powerBasis hf).dim = f.natDegree
-- Mathlib.Algebra.Algebra.NonUnitalHom
AlgHom.instNonUnitalAlgHomClassOfAlgHomClass : ∀ {F : Type u_1} {R : Type u_2} [inst : CommSemiring R] {A : Type u_3} {B : Type u_4} [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : FunLike F A B] [AlgHomClass F R A B],
  NonUnitalAlgHomClass F R A B
-- Init.Data.Int.Order
Int.sub_nonneg : ∀ {a b : ℤ}, 0 ≤ a - b ↔ b ≤ a
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app : ∀ {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] (F : CategoryTheory.Functor C D) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] (X : C)
  (a b : A) (h : a + b = 0),
  F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
        ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)))
-- Mathlib.Analysis.Calculus.FDeriv.Norm
HasStrictFDerivAt.hasStrictFDerivAt_norm_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ},
  t ≠ 0 → HasStrictFDerivAt (fun x => ‖x‖) f x → HasStrictFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ),
  φ.IsHomogeneous n = MvPolynomial.IsWeightedHomogeneous 1 φ n
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplex_X₂ : ∀ {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 j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplex._auto_3),
  (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_star : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], (star a).re = a.re + c₂ * a.imI
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.top_eq_mk_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M},
  ⊤ = MulArchimedeanClass.mk a ↔ a = 1
-- Init.Data.UInt.Lemmas
USize.size_sub_one_mod_uint8Size : (USize.size - 1) % UInt8.size = UInt8.size - 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_eq_getElem! : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α} {h' : a ∈ m}, m[a] = m[a]!
-- Mathlib.MeasureTheory.Measure.Haar.Disintegration
/-- The image of an additive Haar measure under a surjective linear map is proportional to a given
additive Haar measure, with a positive (but maybe infinite) factor.  -/
LinearMap.exists_map_addHaar_eq_smul_addHaar : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [BorelSpace E] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [BorelSpace F] [inst_9 : NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F)
  (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
  [LocallyCompactSpace E], Function.Surjective ⇑L → ∃ c, 0 < c ∧ MeasureTheory.Measure.map (⇑L) μ = c • ν
-- Mathlib.GroupTheory.Frattini
/-- When `G` is finite, the Frattini subgroup is nilpotent.  -/
frattini_nilpotent : ∀ {G : Type u_1} [inst : Group G] [Finite G], Group.IsNilpotent ↥(frattini G)
-- Mathlib.Order.Partition.Equipartition
Finpartition.IsEquipartition.filter_ne_average_add_one_eq_average : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  P.IsEquipartition →
    {p ∈ P.parts | ¬p.card = s.card / P.parts.card + 1} = {p ∈ P.parts | p.card = s.card / P.parts.card}
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inclusion_inj_on_objects : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S T : CategoryTheory.Subgroupoid C} (h : S ≤ T),
  Function.Injective (CategoryTheory.Subgroupoid.inclusion h).obj
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformly.sub : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly G g l → TendstoLocallyUniformly (F - G) (f - g) l
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.addGrpObjObj.eq_1 : ∀ {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]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] {G : C} [inst_5 : CategoryTheory.AddGrpObj G],
  CategoryTheory.Functor.addGrpObjObj =
    { toAddMonObj := CategoryTheory.Functor.addMonObjObj G, neg := F.map CategoryTheory.AddGrpObj.neg, left_neg := ⋯,
      right_neg := ⋯ }
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.compForgetAugmentedIso.eq_1 : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Monoid G],
  Rep.standardComplex.compForgetAugmentedIso k G = CategoryTheory.eqToIso ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- `cfcₙHom` bundled as a continuous linear map.  -/
cfcₙL : {R : Type u_1} →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [inst_4 : IsTopologicalSemiring R] →
                [inst_5 : ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : TopologicalSpace A] →
                        [inst_9 : Module R A] →
                          [inst_10 : IsScalarTower R A A] →
                            [inst_11 : SMulCommClass R A A] →
                              [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] →
                                {a : A} → p a → ContinuousMapZero (↑(quasispectrum R a)) R →L[R] A
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp.mk.sizeOf_spec : ∀ (signatures : Array Lean.Lsp.SignatureInformation) (activeSignature? activeParameter? : Option ℕ),
  sizeOf { signatures := signatures, activeSignature? := activeSignature?, activeParameter? := activeParameter? } =
    1 + sizeOf signatures + sizeOf activeSignature? + sizeOf activeParameter?
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- If `h` is a positive strict period of `f`, then the `q`-expansion coefficient can be expressed
as an integral along a horizontal line in the upper half-plane from `t * I` to `h + t * I`, for
any `0 < t`.
 -/
UpperHalfPlane.qExpansion_coeff_eq_intervalIntegral : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ (n : ℕ) {t : ℝ} (ht : 0 < t),
            (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h f) =
              1 / ↑h *
                ∫ (u : ℝ) in 0..h,
                  1 / Function.Periodic.qParam h (↑u + ↑t * ↑UpperHalfPlane.I) ^ n *
                    f { coe := ↑u + ↑t * ↑UpperHalfPlane.I, coe_im_pos := ⋯ }
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getCast? : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [LawfulBEq α] → (a : α) → Std.DHashMap.Internal.AssocList α β → Option (β a)
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype_lt : ∀ {α : Type u_1} [inst : Fintype α] {p : α → Prop} [inst_1 : Fintype { a // p a }] {x : α},
  ¬p x → Fintype.card { x // p x } < Fintype.card α
-- Mathlib.LinearAlgebra.Projection
Submodule.projectionOnto_surjective : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), Function.Surjective ⇑(p.projectionOnto q h)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α},
  m.WF → (Std.DHashMap.Raw.map f m).contains k = m.contains k
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc.eq_1 : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F),
  AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc F s =
    {
      base :=
        CategoryTheory.Limits.colimit.desc (F.comp (AlgebraicGeometry.PresheafedSpace.forget C))
          ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s),
      c :=
        { app := fun U => AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U, naturality := ⋯ } }
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_smul : ∀ {K : Type u_4} {V : Type u_8} {V₂ : Type u_9} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (a : K), a ≠ 0 → (a • f).range = f.range
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose.eq_3 : ∀ (n k : ℕ), n.succ.multichoose k.succ = n.multichoose (k + 1) + (n + 1).multichoose k
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.mem_skeletonOfMono_obj_iff : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d) {d' : ℕ},
  c.simplex ∈ ((SSet.skeletonOfMono i) d').obj (Opposite.op { len := d }) ↔
    c.simplex ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d }))) ∨ d < d'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushout_inl_inv_inr_of_right_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.inv (CategoryTheory.Limits.pushout.inr f g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv f) g
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty_of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  [AlgebraicGeometry.IsZariskiLocalAtSource P],
  RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] f => P (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f))
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.ext_iff : ∀ {J : Type u_1} {inst : LinearOrder J} {i j : J} {x y : CategoryTheory.SimplicialThickening.Path i j},
  x = y ↔ x.I = y.I
-- Mathlib.Order.Hom.Lattice
SupHom.dual_symm_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Max β] (f : InfHom αᵒᵈ βᵒᵈ) (a : αᵒᵈ),
  (SupHom.dual.symm f) a = f a
-- Mathlib.Order.Filter.Extr
IsMinOn.sup : ∀ {α : Type u} {β : Type v} [inst : SemilatticeSup β] {f g : α → β} {a : α} {s : Set α},
  IsMinOn f s a → IsMinOn g s a → IsMinOn (fun x => f x ⊔ g x) s a
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.isIntCastInst : Lean.Expr → Lean.Meta.Grind.Arith.FieldNormNum.M✝ Bool
-- Mathlib.Computability.Partrec
Partrec.rfind : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → ℕ →. Bool}, Partrec₂ p → Partrec fun a => Nat.rfind (p a)
-- Mathlib.Data.List.Sublists
List.sublists_nil : ∀ {α : Type u}, [].sublists = [[]]
-- Mathlib.Combinatorics.SimpleGraph.Finite
/-- The edges whose vertices lie in `s` are in bijection with the edges of the induced
subgraph `G.induce s`.  -/
SimpleGraph.card_filter_edgeFinset_toFinset_subset : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  (s : Finset V), {e ∈ G.edgeFinset | e.toFinset ⊆ s}.card = (SimpleGraph.induce (↑s) G).edgeFinset.card
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContMDiffAddOfTopWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {a : WithTop ℕ∞} [ContMDiffAdd I ⊤ G],
  ContMDiffAdd I a G
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instMin : {α : Type u_1} → [inst : LE α] → Min (LowerSet α)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.lt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.lt = Ordering.eq → motive Ordering.eq) (h_3 : Ordering.lt = Ordering.gt → motive Ordering.gt),
  (match h : Ordering.lt with
    | Ordering.lt => h_1 h
    | Ordering.eq => h_2 h
    | Ordering.gt => h_3 h) =
    h_1 ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The graded tensor product of two elements of graded rings.  -/
GradedTensorProduct.«term_ᵍ⊗ₜ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
map_multiset_ne_zero_prod : ∀ {F : Type u_1} {M : Type u_5} {N : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] [inst_2 : FunLike F M N]
  [MulHomClass F M N] (f : F) {s : Multiset M}, s ≠ 0 → f s.prod = (Multiset.map (⇑f) s).prod
-- Init.Data.SInt.Lemmas
ISize.lt_of_le_of_ne : ∀ {a b : ISize}, a ≤ b → a ≠ b → a < b
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- The topology on a linearly ordered group with zero element adjoined is compatible with the order
structure: the set `{p : Γ₀ × Γ₀ | p.1 ≤ p.2}` is closed.  -/
WithZeroTopology.orderClosedTopology : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], OrderClosedTopology Γ₀
-- Mathlib.Order.Hom.Bounded
BotHom.instSemilatticeInf : {α : Type u_2} →
  {β : Type u_3} → [inst : Bot α] → [inst_1 : SemilatticeInf β] → [inst_2 : OrderBot β] → SemilatticeInf (BotHom α β)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.val_inv_equivUnitsAffineMap_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (e : P₁ ≃ᵃ[k] P₁), ↑(AffineEquiv.equivUnitsAffineMap e)⁻¹ = ↑e.symm
-- Mathlib.Order.LatticeIntervals
Set.Iic.instBoundedOrderElemOfOrderBot : {α : Type u_1} → {a : α} → [inst : Preorder α] → [OrderBot α] → BoundedOrder ↑(Set.Iic a)
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (X : C) →
          [comon : CategoryTheory.ComonObj X] → [comm : CategoryTheory.IsCommComonObj X] → CategoryTheory.CommComon C
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonChangeAnnotationSupport.fromJson : Lean.Json → Except String Lean.Lsp.ChangeAnnotationSupport
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.coePolynomial_eq_algebraMap : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : Polynomial K),
  ↑p = (algebraMap (Polynomial K) (RatFunc K)) p
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `f : X ⟶ Y` is a morphism between affine schemes, the corresponding arrow is isomorphic
to the arrow of the morphism on prime spectra induced by the map on global sections.  -/
AlgebraicGeometry.arrowIsoSpecΓOfIsAffine : {X Y : AlgebraicGeometry.Scheme} →
  [AlgebraicGeometry.IsAffine X] →
    [AlgebraicGeometry.IsAffine Y] →
      (f : X ⟶ Y) →
        CategoryTheory.Arrow.mk f ≅
          CategoryTheory.Arrow.mk (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f))
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearMap.instIsStablyFiniteRingEnd : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] [IsStablyFiniteRing R], IsStablyFiniteRing (Module.End R M)
-- Init.Data.Range.Polymorphic.SInt
Int64.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int64
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.val_eq_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1}, Metric.Snowflaking.val = ⇑Metric.Snowflaking.ofSnowflaking
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
CategoryTheory.Abelian.FreydMitchell.instFullModuleCatEmbeddingRingFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  (CategoryTheory.Abelian.FreydMitchell.functor C).Full
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Ordered.min?_le : ∀ {α : Type u_1} {cmp : α → α → Ordering} {a : α} {t : RBTree.RBNode α} [Std.TransCmp cmp],
  RBTree.RBNode.Ordered cmp t → t.min? = some a → ∀ x ∈ t, cmp a x ≠ Ordering.gt
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonDidSaveTextDocumentParams : Lean.ToJson Lean.Lsp.DidSaveTextDocumentParams
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSlice.instToIterator : {α : Type u_1} →
  {β : α → Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.RciSliceData α β)) Id (Std.DTreeMap.Internal.Zipper α β)
        ((a : α) × β a)
-- Mathlib.LinearAlgebra.Span.Basic
/-- **Alias** of `Submodule.map_span_le`. -/
LinearMap.map_span_le : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : Set M) (N : Submodule R₂ M₂),
  Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0`, `+`, unary `-`, and binary
`-` is a `SubtractionCommMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`,
and binary `-` to a `SubtractionCommMonoid`. This version takes custom `nsmul` and `zsmul` as
`[SMul ℕ M₁]` and `[SMul ℤ M₁]` arguments.  -/
Function.Injective.subtractionCommMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : Neg M₁] →
            [inst_4 : Sub M₁] →
              [inst_5 : SMul ℤ M₁] →
                [inst_6 : SubtractionCommMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → SubtractionCommMonoid M₁
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.mapsTo_cos : ∀ (s : Set ℝ), Set.MapsTo Real.cos s (Set.Icc (-1) 1)
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_intCast : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (i : ℤ), WittVector.ghostFun✝ ↑i = ↑i
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.toIsTopologicalRing : ∀ {R : Type u} [inst : Ring R] (self : RingTopology R), IsTopologicalRing R