mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.tmul_algebraMap_mul_coe_tmul : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {i₂ : ι} (a₁ : A) (r : R) (a₂ : ↥(𝒜 i₂)) (b₂ : B),
  a₁ ᵍ⊗ₜ[R] (algebraMap R B) r * ↑a₂ ᵍ⊗ₜ[R] b₂ = (a₁ * ↑a₂) ᵍ⊗ₜ[R] ((algebraMap R B) r * b₂)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.triangle : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] (d : PseudoMetric X R) (x y z : X),
  d x z ≤ d x y + d y z
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The homotopy between `pathObject.ι₀ K` and `pathObject.ι₁ K`.  -/
HomologicalComplex.pathObject.homotopy₀₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] →
                  (∀ (i : α), ∃ j, c.Rel i j) →
                    Homotopy (HomologicalComplex.pathObject.π₀ K) (HomologicalComplex.pathObject.π₁ K)
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Eventually.intCast_atBot : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop},
  (∀ᶠ (x : R) in Filter.atBot, p x) → ∀ᶠ (n : ℤ) in Filter.atBot, p ↑n
-- Init.Data.Int.Order
Int.natAbs_add_of_nonpos : ∀ {a b : ℤ}, a ≤ 0 → b ≤ 0 → (a + b).natAbs = a.natAbs + b.natAbs
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.coeff_expand_of_not_dvd : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {p : ℕ} (φ : MvPolynomial σ R) {m : σ →₀ ℕ} {i : σ},
  ¬p ∣ m i → MvPolynomial.coeff m ((MvPolynomial.expand p) φ) = 0
-- Init.Core
/-- `insert x xs` inserts the element `x` into the collection `xs`.  -/
Insert.insert : {α : outParam (Type u)} → {γ : Type v} → [self : Insert α γ] → α → γ → γ
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
HomotopicalAlgebra.FibrantObject.instIsConnectedRightResolutionWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  CategoryTheory.IsConnected ((HomotopicalAlgebra.FibrantObject.localizerMorphism C).RightResolution X)
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Auxiliary definition for `mk`.  -/
ChainComplex.mkAux : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (X₀ X₁ X₂ : V) →
        (d₀ : X₁ ⟶ X₀) →
          (d₁ : X₂ ⟶ X₁) →
            CategoryTheory.CategoryStruct.comp d₁ d₀ = 0 →
              ((S : CategoryTheory.ShortComplex V) →
                  (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0) →
                ℕ → CategoryTheory.ShortComplex V
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
Polynomial.exists_irreducible_of_natDegree_ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [NoZeroDivisors R] [WfDvdMonoid R] {f : Polynomial R} [Nontrivial R],
  f.natDegree ≠ 0 → ∃ g, Irreducible g ∧ g ∣ f
-- Mathlib.Tactic.Order.Graph.Basic
/-- Source of the edge.  -/
Mathlib.Tactic.Order.Edge.src : Mathlib.Tactic.Order.Edge → ℕ
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.HasProp.hasProp : ∀ {P : TopCat → Prop} {X : Type u} {inst : TopologicalSpace X} [self : CompHausLike.HasProp P X], P (TopCat.of X)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubOffset_6 : HSub Std.Time.Timestamp Std.Time.Nanosecond.Offset Std.Time.Timestamp
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : β → γ}, ProbabilityTheory.Kernel.map 0 f = 0
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_lt_iff_lt : ∀ {a b : ℕ} (ha : a < UInt64.size) (hb : b < UInt64.size), UInt64.ofNatLT a ha < UInt64.ofNatLT b hb ↔ a < b
-- Plausible.DeriveShrinkable
/-- Derives a `Shrinkable` instance for a single inductive type  -/
_private.Plausible.DeriveShrinkable.0.Plausible.mkShrinkableInstanceCmd : Lean.Name → Lean.Elab.TermElabM (Array Lean.Syntax)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.below.nil : ∀ {motive : (m : ℕ) → (L : List ℕ) → SimplexCategoryGenRel.IsAdmissible m L → Prop} (m : ℕ),
  SimplexCategoryGenRel.IsAdmissible.below ⋯
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharType.upper.sizeOf_spec : sizeOf Lean.FuzzyMatching.CharType.upper = 1
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Increment.0.SzemerediRegularity.distinctPairs_increment : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
  P.parts.offDiag.attach.biUnion (SzemerediRegularity.distinctPairs✝ hP G ε) ⊆
    (SzemerediRegularity.increment hP G ε).parts.offDiag
-- Mathlib.Order.Hom.Basic
OrderIso.refl_toEquiv : ∀ {α : Type u_2} [inst : LE α], (OrderIso.refl α).toEquiv = Equiv.refl α
-- Mathlib.Data.FunLike.Basic
DFunLike.ite_apply : ∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α β] {P : Prop} [inst : Decidable P] (f g : F) (x : α),
  (if P then f else g) x = if P then f x else g x
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι),
  P.pairingIn ℤ (RootPairing.EmbeddedG2.twoShortAddLong P) i =
    2 * P.pairingIn ℤ (RootPairing.EmbeddedG2.short P) i + P.pairingIn ℤ (RootPairing.EmbeddedG2.long P) i
-- Mathlib.Order.Sublocale
Sublocale.carrier.instInfSet : {X : Type u_1} → [inst : Order.Frame X] → {S : Sublocale X} → InfSet ↥S
-- Mathlib.Order.Heyting.Basic
PUnit.instBiheytingAlgebra : BiheytingAlgebra PUnit.{u + 1}
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localAlgEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] [inst_4 : Algebra R P] (I : Ideal S) [inst_5 : I.IsPrime] (J : Ideal P) [inst_6 : J.IsPrime]
  (f : S ≃ₐ[R] P) (hIJ : I = Ideal.comap f J) (a : Localization.AtPrime I),
  (Localization.localAlgEquiv I J f hIJ) a = (↑↑(Localization.localAlgHom I J (↑f) hIJ).toRingHom).toFun a
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr.beq.eq_2 : ∀ (x x_1 : Nat.Internal.Linear.PolyCnstr),
  (∀ (a : Bool) (a_1 a_2 : Nat.Internal.Linear.Poly) (b : Bool) (b_1 b_2 : Nat.Internal.Linear.Poly),
      x = { eq := a, lhs := a_1, rhs := a_2 } → x_1 = { eq := b, lhs := b_1, rhs := b_2 } → False) →
    Nat.Internal.Linear.instBEqPolyCnstr.beq x x_1 = false
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.params : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.FunDecl pu → Array (Lean.Compiler.LCNF.Param pu)
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.pow_card_sub_one_eq_one : ∀ {K : Type u_1} [inst : GroupWithZero K] [inst_1 : Fintype K] (a : K), a ≠ 0 → a ^ (Fintype.card K - 1) = 1
-- Mathlib.Topology.Separation.Basic
subsingleton_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X}, (closure s).Subsingleton ↔ s.Subsingleton
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberDesc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P : CategoryTheory.Functor Cᵒᵖ A} {T : A}
  (φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T))
  (hφ :
    autoParam
      (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
        CategoryTheory.CategoryStruct.comp (P.map f.op) (φ X x) =
          φ Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x))
      _auto_52✝)
  (X : C) (x : Φ.fiber.obj X) {Z : A} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P)
      (CategoryTheory.CategoryStruct.comp (Φ.presheafFiberDesc φ hφ) h) =
    CategoryTheory.CategoryStruct.comp (φ X x) h
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.prod_rcons : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : (i : ι) → DecidableEq (M i)] {i : ι}
  (p : Monoid.CoprodI.Word.Pair M i), (Monoid.CoprodI.Word.rcons p).prod = Monoid.CoprodI.of p.head * p.tail.prod
-- Mathlib.RingTheory.Kaehler.Basic
/-- The map `I → B ⊗[A] Ω[A⁄R]` where `I = ker(A → B)`.  -/
KaehlerDifferential.kerToTensor : (R : Type u) →
  [inst : CommRing R] →
    (A : Type u_2) →
      (B : Type u_3) →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra A B] → ↥(RingHom.ker (algebraMap A B)) →ₗ[A] TensorProduct A B Ω[A⁄R]
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.IsRingHom.comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {R₁ R₂ R₃ : C} [inst_2 : CategoryTheory.AddMonObj R₁] [inst_3 : CategoryTheory.AddMonObj R₂]
  [inst_4 : CategoryTheory.AddMonObj R₃] [inst_5 : CategoryTheory.MonObj R₁] [inst_6 : CategoryTheory.MonObj R₂]
  [inst_7 : CategoryTheory.MonObj R₃] (f : R₁ ⟶ R₂) (g : R₂ ⟶ R₃) [CategoryTheory.IsRingHom f]
  [CategoryTheory.IsRingHom g], CategoryTheory.IsRingHom (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.Context.mk : List Lean.FVarId → Lean.Meta.RefinedDiscrTree.Context✝
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.comap.congr_simp : ∀ {R : Type u} [inst : CommRing R] {S : Type u} [inst_1 : CommRing S] (f f_1 : R →+* S) (e_f : f = f_1)
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S))
  (hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier),
  AlgebraicGeometry.StructureSheaf.comap f U V hUV = AlgebraicGeometry.StructureSheaf.comap f_1 U V ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.list_sum_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {L : List A}, (∀ x ∈ L, x ∈ S) → L.sum ∈ S
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerLeft_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ)
  {b c : B} {a' : C} (f : a' ⟶ F.obj b) (g : b ⟶ c) {Z : a' ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (θ.app b) (G.map g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (F.map g) (Γ.app c)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (η.naturality g).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (Γ.app b) (G.map g))) h)
-- Mathlib.CategoryTheory.Join.Pseudofunctor
/-- The structural isomorphism for composition of `pseudofunctorRight`.  -/
CategoryTheory.Join.mapCompRight : (A : Type u_1) →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (F : CategoryTheory.Functor B C) →
                  (G : CategoryTheory.Functor C D) →
                    CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) (F.comp G) ≅
                      (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).comp
                        (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) G)
-- Mathlib.Algebra.Category.ModuleCat.AB
instAB4ModuleCat : ∀ (R : Type u) [inst : Ring R], CategoryTheory.AB4 (ModuleCat R)
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.instInhabitedDSimpM : {α : Type} → Inhabited (Lean.Meta.Sym.DSimp.DSimpM α)
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getKeyD : {α : Type u} → {β : α → Type v} → [BEq α] → α → α → Std.DHashMap.Internal.AssocList α β → α
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHomEq_inv_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f g : T₁ ⟶ T₂} (h : f = g)
  (X : T₂.Algebra),
  ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).inv.app X).f =
    (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).inv
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_null : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] (a : α),
  MeasurableSet s → (((κ.compProd η) a) s = 0 ↔ (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0)
-- Batteries.Data.Array.Merge
_private.Batteries.Data.Array.Merge.0.Array.mergeDedupWith.go.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A point in the `affineSpan` of a subset of an indexed family is an
`affineCombination` with sum of weights 1, using only points in the given subset.  -/
eq_affineCombination_of_mem_affineSpan_image : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] {p₁ : P} {p : ι → P} {s : Set ι},
  p₁ ∈ affineSpan k (p '' s) → ∃ fs w, ↑fs ⊆ s ∧ ∑ i ∈ fs, w i = 1 ∧ p₁ = (Finset.affineCombination k fs p) w
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_algebraMap : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : Polynomial K),
  (RatFunc.liftRingHom φ hφ) ((algebraMap (Polynomial K) (RatFunc K)) x) = φ x
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The right inclusion `(K ⊞ K).X i ⟶ K.cylinder.X i`.  -/
HomologicalComplex.cylinder.inrX : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] → (i : ι) → (K ⊞ K).X i ⟶ K.cylinder.X i
-- Mathlib.Algebra.Module.LocalizedModule.Basic
isLocalizedModule_id : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (M : Type u_2) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (R' : Type u_6) [inst_3 : CommSemiring R'] [inst_4 : Algebra R R'] [IsLocalization S R']
  [inst_6 : Module R' M] [IsScalarTower R R' M], IsLocalizedModule S LinearMap.id
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instBEqSemanticTokenType.beq : Lean.Lsp.SemanticTokenType → Lean.Lsp.SemanticTokenType → Bool
-- Lean.Structure
Lean.StructureDescr.mk.inj : ∀ {structName : Lean.Name} {fields : Array Lean.StructureFieldInfo} {structName_1 : Lean.Name}
  {fields_1 : Array Lean.StructureFieldInfo},
  { structName := structName, fields := fields } = { structName := structName_1, fields := fields_1 } →
    structName = structName_1 ∧ fields = fields_1
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.DescendsAlong.of_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q W : CategoryTheory.MorphismProperty C}
  [P.DescendsAlong Q], W ≤ Q → P.DescendsAlong W
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- Eta-expanded form of `MeasureTheory.Integrable.smul_enorm` -/
MeasureTheory.Integrable.fun_smul_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} {ε : Type u_9}
  [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε] [inst_2 : NormedAddCommGroup 𝕜] [inst_3 : SMul 𝕜 ε]
  [ContinuousConstSMul 𝕜 ε] [ENormSMulClass 𝕜 ε] (c : 𝕜) {f : α → ε},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun i => c • f i) μ
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.card_fixedPoints : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (σ : Equiv.Perm α),
  Fintype.card ↑(Function.fixedPoints ⇑σ) = Fintype.card α - σ.cycleType.sum
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.toList : {α : outParam (Type u)} →
  {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → β → Std.Sat.CNF.Clause α
-- Init.Data.Fin.Lemmas
Fin.sub_val_of_le : ∀ {n : ℕ} {a b : Fin n}, b ≤ a → ↑(a - b) = ↑a - ↑b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constInsertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} [Std.TransOrd α] {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit} (h₁ : t₁.WF)
  (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {l : List α},
      (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t₁ l ⋯)).Equiv
        ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t₂ l ⋯)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- An auxiliary lemma that shows there exists a factorization as a P_δ followed by a P_σ for
morphisms of the form `P_δ ≫ σ`.  -/
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono.0.SimplexCategoryGenRel.factor_P_δ_σ : ∀ {n : ℕ} (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ SimplexCategoryGenRel.mk (n + 1)),
  SimplexCategoryGenRel.P_δ f →
    ∃ z e m,
      ∃ (_ : SimplexCategoryGenRel.P_σ e) (_ : SimplexCategoryGenRel.P_δ m),
        CategoryTheory.CategoryStruct.comp f (SimplexCategoryGenRel.σ i) = CategoryTheory.CategoryStruct.comp e m
-- Mathlib.Topology.Instances.ZMod
/-- The discrete topology (every set is open).  -/
ZMod.instTopologicalSpace : {N : ℕ} → TopologicalSpace (ZMod N)
-- Mathlib.FieldTheory.AxGrothendieck
FirstOrder.realize_genericPolyMapSurjOnOfInjOn : ∀ {ι : Type u_1} {α : Type u_2} [inst : Finite α] {K : Type u_3} [inst_1 : Field K]
  [inst_2 : FirstOrder.Ring.CompatibleRing K] [inst_3 : Finite ι] (φ : FirstOrder.Language.ring.Formula (α ⊕ ι))
  (mons : ι → Finset (ι →₀ ℕ)),
  K ⊨ FirstOrder.genericPolyMapSurjOnOfInjOn φ mons ↔
    ∀ (v : α → K) (p : { p // ∀ (i : ι), (p i).support ⊆ mons i }),
      have f := fun v i => (MvPolynomial.eval v) (↑p i);
      have S := {x | φ.Realize (Sum.elim v x)};
      Set.MapsTo f S S → Set.InjOn f S → Set.SurjOn f S S
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.Repr.induced_left : ∀ {R : Type u} {A : Type v} {B : Type w} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A]
  [inst_6 : Coalgebra R B] {a : A} (repr : Coalgebra.Repr R a ι) {F : Type u_2} [inst_7 : FunLike F A B]
  [inst_8 : CoalgHomClass F R A B] (φ : F) (a_1 : ι), (repr.induced φ).left a_1 = (⇑φ ∘ repr.left) a_1
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {a a' : α}, m.WF → m.getKey? a = some a' → a' ∈ m
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.mon_tauto_proc : Lean.ParserDescr
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.length_map : ∀ {α : Type u_1} {β : Type u_2} {as : List α} (f : α → β), (List.map f as).length = as.length
-- Mathlib.Data.List.Basic
List.foldr_fixed : ∀ {α : Type u} {β : Type v} {b : β} (l : List α), List.foldr (fun x b => b) b l = b
-- Mathlib.Data.Fin.Rev
Fin.revPerm_apply : ∀ {n : ℕ} (i : Fin n), Fin.revPerm i = i.rev
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (∀ (k' : α), t.maxKey? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.bound_pos : ∀ (ε : ℝ) (l : ℕ), 0 < SzemerediRegularity.bound ε l
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.diagram : {J : Type u₁} → J → CategoryTheory.Bicone J
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.isSolvable_tensorProduct_iff : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u_1}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [Module.FaithfullyFlat R A],
  LieAlgebra.IsSolvable (TensorProduct R A L) ↔ LieAlgebra.IsSolvable L
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank.eq_1 : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] (A : Matrix m n R), A.eRank = Cardinal.toENat A.cRank
-- Init.Data.Range.Polymorphic.RangeIterator
/-- Internal state of the range iterators. Do not depend on its internals.  -/
Std.Rxi.Iterator : Type u → Type u
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.map_subtype_le : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  (p' : Submodule R ↥p), Submodule.map p.subtype p' ≤ p