mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.mk.sizeOf_spec : ∀ {P : Type u_2} [inst : Preorder P] [inst_1 : SizeOf P] (I : Order.Ideal P) (F : Order.PFilter P)
  (isCompl_I_F : IsCompl ↑I ↑F),
  sizeOf { I := I, F := F, isCompl_I_F := isCompl_I_F } = 1 + sizeOf I + sizeOf F + sizeOf isCompl_I_F
-- Mathlib.Logic.Function.Basic
Function.instIsPreorderSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsPreorder α r], IsPreorder α (Function.swap r)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
/-- If `X` is a colimit indexed by `J` of objects satisfying a property `P`, then
any object that is isomorphic to `X` also is.  -/
CategoryTheory.ObjectProperty.ColimitOfShape.ofIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {P : CategoryTheory.ObjectProperty C} →
      {J : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} J] →
          {X : C} → P.ColimitOfShape J X → {Y : C} → (X ≅ Y) → P.ColimitOfShape J Y
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.coe_eq_coe : ∀ {α : Type u} [inst : TopologicalSpace α] {x y : α},
  ConnectedComponents.mk x = ConnectedComponents.mk y ↔ connectedComponent x = connectedComponent y
-- Mathlib.Analysis.Normed.Operator.Banach
/-- A choice of continuous left inverse of an injective continuous linear map with closed range:
this is `LinearMap.leftInverse` as a continuous linear map;
by injectivity, the junk value of `leftInverse` never matters, and continuity of the inverse
follows form the closed range condition.  -/
ContinuousLinearMap.leftInverse_of_injective_of_isClosed_range : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_5} →
      {F : Type u_6} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                [CompleteSpace E] →
                  [CompleteSpace F] →
                    (f : E →L[𝕜] F) → Function.Injective ⇑f → IsClosed (Set.range ⇑f) → ↥(↑f).range →L[𝕜] E
-- Mathlib.Data.Finset.NoncommProd
Finset.map_noncommProd : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Monoid β] [inst_1 : Monoid γ]
  [inst_2 : FunLike F β γ] [inst_3 : MonoidHomClass F β γ] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun Commute f)) (g : F),
  g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
ContinuousMapZero.UniqueHom.congr_simp : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : NonUnitalRing A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Module R A] [inst_9 : IsScalarTower R A A] [inst_10 : SMulCommClass R A A],
  ContinuousMapZero.UniqueHom R A = ContinuousMapZero.UniqueHom R A
-- Mathlib.Algebra.Group.Subgroup.Actions
AddSubgroup.instFaithfulVAddSubtypeMem : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] [FaithfulVAdd G α] (S : AddSubgroup G),
  FaithfulVAdd (↥S) α
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteVerts_empty : ∀ {α : Type u_1} {β : Type u_2} (G : Graph α β), G.deleteVerts ∅ = G
-- Mathlib.Tactic.FunProp.Elab
/-- Tactic to prove function properties  -/
Mathlib.Meta.FunProp.funPropTac : Lean.Elab.Tactic.Tactic
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.HasFiniteIntegral.restrict_of_bounded : ∀ {α : Type u_1} {E : Type u_5} {mα : MeasurableSpace α} [inst : NormedAddCommGroup E] {f : α → E} {s : Set α}
  {μ : MeasureTheory.Measure α} (C : ℝ),
  μ s < ⊤ → (∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C) → MeasureTheory.HasFiniteIntegral f (μ.restrict s)
-- Init.Data.UInt.Lemmas
UInt64.le_of_lt : ∀ {a b : UInt64}, a < b → a ≤ b
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInlCompAssociator_hom_app_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : C),
  ((CategoryTheory.sum.inlCompInlCompAssociator C D E).hom.app X).down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inl X)).down
      (CategoryTheory.CategoryStruct.id (Sum.inl X)).down
-- Std.Http.Data.Request
/-- Adds a single header to the request being built, panics if the header is invalid.
 -/
Std.Http.Request.Builder.header! : Std.Http.Request.Builder → String → String → Std.Http.Request.Builder
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- a choice of kernel of the induced morphism `S.g' : S.Q ⟶ X₃`  -/
CategoryTheory.ShortComplex.RightHomologyData.H : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → {S : CategoryTheory.ShortComplex C} → S.RightHomologyData → C
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.ShortExact → S.Exact
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.mem_center_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {z : M}, z ∈ AddSubmonoid.center M ↔ ∀ (g : M), g + z = z + g
-- Init.Data.SInt.Lemmas
instLawfulIdentityInt8HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Algebra.Group.Hom.Defs
OneHomClass.mk : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} [inst : One M] [inst_1 : One N]
  [inst_2 : FunLike F M N], (∀ (f : F), f 1 = 1) → OneHomClass F M N
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProdRight_apply : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a : α) (snd : β),
  (G.boxProdRight H a) snd = (a, snd)
-- Lean.Level
Lean.Level.param.sizeOf_spec : ∀ (a : Lean.Name), sizeOf (Lean.Level.param a) = 1 + sizeOf a
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- We have that `λ` divides `x * (x - 1) * (x - (η + 1))`.  -/
IsCyclotomicExtension.Rat.Three.lambda_dvd_mul_sub_one_mul_sub_eta_add_one : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) (x : NumberField.RingOfIntegers K)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K], hζ.toInteger - 1 ∣ x * (x - 1) * (x - (↑⋯.unit + 1))
-- Mathlib.Analysis.Normed.Group.Constructions
pi_nnnorm_const_le' : ∀ {ι : Type u_1} {E : Type u_2} [inst : Fintype ι] [inst_1 : SeminormedGroup E] (a : E), ‖fun x => a‖₊ ≤ ‖a‖₊
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor preserving larger cofiltered limits also preserves smaller cofiltered limits.  -/
CategoryTheory.Limits.preservesCofilteredLimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Mathlib.Algebra.Order.Module.Pointwise
lowerBounds_smul_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β]
  {s : Set β} {a : α}, a < 0 → lowerBounds (a • s) = a • upperBounds s
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, MeasurableSet s → MeasureTheory.Measure.count s = ↑s.encard
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from types to its "nat module id". We cache failures using `none`.
`natTypeIdOf[type]` is `some id`, then `id < natStructs.size`.
If a type is in this map, it is not in `typeIdOf`.
 -/
Lean.Meta.Grind.Arith.Linear.State.natTypeIdOf : Lean.Meta.Grind.Arith.Linear.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
Disjoint.edgeSet : ∀ {V : Type u} {G : SimpleGraph V} {H₁ H₂ : G.Subgraph}, Disjoint H₁ H₂ → Disjoint H₁.edgeSet H₂.edgeSet
-- Mathlib.CategoryTheory.Preadditive.Projective.Internal
/-- An object `P : C` is *internally projective* if the functor `P ⟶[C] -` taking internal homs
out of `P` preserves epimorphisms.
 -/
CategoryTheory.InternallyProjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.MonoidalClosed C] → C → Prop
-- Init.Data.List.Basic
List.filter.eq_1 : ∀ {α : Type u} (p : α → Bool), List.filter p [] = []
-- Mathlib.Analysis.Complex.Exponential
_private.Mathlib.Analysis.Complex.Exponential.0.Real.add_one_lt_exp_of_pos : ∀ {x : ℝ}, 0 < x → x + 1 < Real.exp x
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Expr.updateProjS! : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Lean.Expr → m Lean.Expr
-- Lean.Environment
/-- Like `findRec?`; allocating tasks is (currently?) too costly to do always.  -/
_private.Lean.Environment.0.Lean.AsyncConsts.findRecTask : Lean.AsyncConsts✝ → Lean.Name → Task (Option Lean.AsyncConst✝)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset : ∀ {α : 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 : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) [inst_4 : MeasurableSpace E]
  [inst_5 : BorelSpace E] {f : α → E} (fmeas : Measurable f),
  MeasureTheory.Integrable f μ →
    ∀ (s : Set E) [inst_6 : TopologicalSpace.SeparableSpace ↑s] (hs : Set.range f ∪ {0} ⊆ s),
      Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT ⇑(MeasureTheory.SimpleFunc.approxOn f fmeas s 0 ⋯ n))
        Filter.atTop (nhds (MeasureTheory.setToFun μ T hT f))
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₂_of_isCharThreeJNeZeroNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3], W.b₂ = W.a₂
-- Mathlib.Data.Fintype.EquivFin
/-- Two `Fintype`s with the same cardinality are (computably) in bijection.

See `Fintype.equivOfCardEq` for the noncomputable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq` for
the specialization to `Fin`.
 -/
Fintype.truncEquivOfCardEq : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Fintype α] →
      [inst_1 : Fintype β] → [DecidableEq α] → [DecidableEq β] → Fintype.card α = Fintype.card β → Trunc (α ≃ β)
-- Mathlib.NumberTheory.Bertrand
/-- **Bertrand's Postulate**: For any positive natural number, there is a prime which is greater than
it, but no more than twice as large.
 -/
Nat.exists_prime_lt_and_le_two_mul : ∀ (n : ℕ), n ≠ 0 → ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.nondegenerate_flip_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.flip.Nondegenerate ↔ B.Nondegenerate
-- Init.Data.Random
/-- Interface for random number generators.  -/
RandomGen : Type u → Type u
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.epi_iff_surjective : ∀ {A B : AddCommGrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j k l : ι}
  (_w₁ _w₁_1 : Monoid.CoprodI.NeWord M i j),
  _w₁ = _w₁_1 →
    ∀ (_hne : j ≠ k) (_w₂ _w₂_1 : Monoid.CoprodI.NeWord M k l),
      _w₂ = _w₂_1 → _w₁.append _hne _w₂ = _w₁_1.append _hne _w₂_1
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_X_pow_eq_C_mul : ∀ {R : Type u} [inst : CommSemiring R] (n k : ℕ),
  (⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = Polynomial.C ↑(n.descFactorial k) * Polynomial.X ^ (n - k)
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Dense.extend_exists : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set α} {f : ↑s → β}
  [CompleteSpace β],
  Dense s → UniformContinuous f → ∀ (a : α), ∃ b, Filter.Tendsto f (Filter.comap Subtype.val (nhds a)) (nhds b)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.instInhabitedStruct.default : Lean.Meta.Grind.AC.Struct
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.insertMany_eq_insertListₘ_toListModel : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m m₂ : Std.DHashMap.Internal.Raw₀ α β),
  ↑(m.insertMany ↑m₂) = m.insertListₘ (Std.DHashMap.Internal.toListModel (↑m₂).buckets)
-- Mathlib.RingTheory.PowerSeries.Order
PowerSeries.order_prod : ∀ {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type u_3} (φ : ι → PowerSeries R)
  (s : Finset ι), (∏ i ∈ s, φ i).order = ∑ i ∈ s, (φ i).order
-- Lean.Server.FileWorker.ExampleHover
/-- Adds a comment marker `-- ` to a line in an output code block, respecting indentation, if the line
contains any non-space characters. Lines containing only spaces are returned unmodified.

The comment marker is always added at the indicated indentation. If the content of the line is at
least as indented, then its relative indentation is preserved. Otherwise, it's placed just after the
line comment marker.
 -/
_private.Lean.Server.FileWorker.ExampleHover.0.Lean.Server.FileWorker.Hover.addCommentAt : ℕ → String → String
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.lift_σ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Z : C}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.diag X))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.NonPreadditiveAbelian.r X)) h)) =
    h
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The monoid isomorphism between endomorphisms of `F` and the (multiplicative opposite of the)
limit of automorphism groups of all Galois objects.  -/
CategoryTheory.PreGaloisCategory.endMulEquivAutGalois : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          CategoryTheory.End F ≃* (CategoryTheory.PreGaloisCategory.AutGalois F)ᵐᵒᵖ
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.sum_slash : ∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} {ι : Type u_4} [inst : Monoid G] [inst_1 : AddCommGroup α]
  [inst_2 : SlashAction β G α] (k : β) (g : G) {a : ι → α} {s : Finset ι},
  SlashAction.map k g (∑ i ∈ s, a i) = ∑ i ∈ s, SlashAction.map k g (a i)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Fork.unop_ι_app_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Fork f g),
  c.unop.ι.app CategoryTheory.Limits.WalkingParallelPair.one =
    (c.π.app CategoryTheory.Limits.WalkingParallelPair.zero).unop
-- Mathlib.Topology.PartialHomeomorph.Basic
/-- The inclusion of an subset `s` of a space `X` into `X` is a partial homeomorphism
from the subtype `s` to `X`.  -/
Set.partialHomeomorphSubtypeCoe : {X : Type u_1} → [inst : TopologicalSpace X] → (s : Set X) → Nonempty ↑s → PartialHomeomorph (↑s) X
-- Mathlib.CategoryTheory.MorphismProperty.Descent
/-- Alternative constructor for `CodescendsAlong` using `HasPushout`.  -/
CategoryTheory.MorphismProperty.CodescendsAlong.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C}
  [P.RespectsIso],
  (∀ {X Y Z : C} {f : Z ⟶ X} {g : Z ⟶ Y} [inst_2 : CategoryTheory.Limits.HasPushout f g],
      Q f → P (CategoryTheory.Limits.pushout.inl f g) → P g) →
    P.CodescendsAlong Q
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_one : Real.sqrtTwoAddSeries 0 1 = √2
-- Mathlib.Topology.UniformSpace.Basic
/-- Open elements `s : SetRel α α` of `𝓤 α` such that `(x, y) ∈ s ↔ (y, x) ∈ s` form a basis
of `𝓤 α`.  -/
uniformity_hasBasis_open_symmetric : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V ∧ V.IsSymm) id
-- Mathlib.Control.Traversable.Instances
Option.naturality : ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative G]
  (η : ApplicativeTransformation F G) [LawfulApplicative F] {α : Type u_1} {β : Type u} (f : α → F β) (x : Option α),
  (fun {α} => η.app α) (Option.traverse f x) = Option.traverse ((fun {α} => η.app α) ∘ f) x
-- Mathlib.Order.Filter.Map
Filter.bind_inf_principal : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : α → Filter β} {s : Set β},
  (f.bind fun x => g x ⊓ Filter.principal s) = f.bind g ⊓ Filter.principal s
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.congr_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → (t₁.Equiv t₃ ↔ t₂.Equiv t₃)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.Def.valueTypeName : {γ : Type} → Lean.KeyedDeclsAttribute.Def γ → Lean.Name
-- Mathlib.Algebra.Module.Submodule.LinearMap
Module.End.pow_apply_mem_of_forall_mem : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {f' : M →ₗ[R] M}
  {p : Submodule R M} (n : ℕ), (∀ x ∈ p, f' x ∈ p) → ∀ x ∈ p, (f' ^ n) x ∈ p
-- Mathlib.RingTheory.Localization.Basic
Localization.algHom_ext : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (W : Submonoid A) {f g : Localization W →ₐ[R] B},
  f.comp (Algebra.algHom R A (Localization W)) = g.comp (Algebra.algHom R A (Localization W)) → f = g
-- Init.Ext
Array.ext_iff : ∀ {α : Type u} {xs ys : Array α},
  xs = ys ↔ xs.size = ys.size ∧ ∀ (i : ℕ) (hi₁ : i < xs.size) (hi₂ : i < ys.size), xs[i] = ys[i]
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isMulCocycle₁_of_mem_cocycles₁ : ∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M],
  ∀ f ∈ groupCohomology.cocycles₁ (Rep.ofMulDistribMulAction G M), groupCohomology.IsMulCocycle₁ (⇑Additive.toMul ∘ f)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_sup : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l l' : Filter α}, f =o[l ⊔ l'] g ↔ f =o[l] g ∧ f =o[l'] g
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- Define the conjugation (`star`) of a multiplicative character by conjugating pointwise.  -/
MulChar.starComp : {R : Type u_1} →
  {R' : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing R'] → [StarRing R'] → MulChar R R' → MulChar R R'
-- Init.Data.Dyadic.Basic
Dyadic.toRat.eq_1 : Dyadic.zero.toRat = 0
-- Mathlib.Algebra.Star.Unitary
Unitary.coe_isStarNormal : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (u : ↥(unitary R)), IsStarNormal ↑u
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.one_eq : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [Nontrivial A], spectrum 𝕜 1 = {1}
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.anyM_eq_forIn : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Std.Iter.anyM p it =
    forIn it false fun x x_1 => do
      let __do_lift ← p x
      if __do_lift = true then pure (ForInStep.done true) else pure (ForInStep.yield false)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.iff_of_algEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T), Algebra.QuasiFinite R S ↔ Algebra.QuasiFinite R T
-- Mathlib.Algebra.Order.GroupWithZero.Basic
Left.neg_of_mul_neg_left : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α], a * b < 0 → 0 ≤ b → a < 0
-- Init.Data.Nat.Basic
Nat.sub_one_add_one_eq_of_pos : ∀ {n : ℕ}, 0 < n → n - 1 + 1 = n
-- Init.Data.Range.Polymorphic.Basic
/-- This typeclass ensures that a `HasSize` instance returns the correct size for all ranges.
 -/
Std.Rxo.LawfulHasSize : (α : Type u) → [LT α] → [Std.PRange.UpwardEnumerable α] → [Std.Rxo.HasSize α] → Prop
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `mk_penultimate_end_eq_getLast_edges` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.getLast_edges_eq_mk_penultimate_end : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hp : p.edges ≠ []),
  p.edges.getLast hp = s(p.penultimate, w)
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.incomplete : ByteSlice → ℕ → Std.Http.Protocol.H1.TakeResult
-- Std.Data.ExtDTreeMap.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.ExtDTreeMap.all : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → ((a : α) → β a → Bool) → Bool
-- Mathlib.GroupTheory.Index
AddMonoidHom.finite_iff_finite_ker_range : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (f : G →+ G'),
  Finite G ↔ Finite ↥f.ker ∧ Finite ↥f.range
-- Init.MetaTypes
Lean.Meta.Command.ReduceConfig.mk.sizeOf_spec : ∀ (types proofs implicits : Bool) (transparency : Lean.Meta.TransparencyMode)
  (smartUnfolding check ignoreStuckTC : Bool),
  sizeOf
      { types := types, proofs := proofs, implicits := implicits, transparency := transparency,
        smartUnfolding := smartUnfolding, check := check, ignoreStuckTC := ignoreStuckTC } =
    1 + sizeOf types + sizeOf proofs + sizeOf implicits + sizeOf transparency + sizeOf smartUnfolding + sizeOf check +
      sizeOf ignoreStuckTC
-- Mathlib.Order.WellFoundedSet
Set.IsWF.of_wellFoundedLT : ∀ {α : Type u_2} [inst : LT α] [h : WellFoundedLT α] (s : Set α), s.IsWF
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the second of three points is strictly between the other two, the angle at the third point
(reversed) is zero.  -/
Sbtw.angle₁₃₂_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, Sbtw ℝ p₁ p₂ p₃ → EuclideanGeometry.angle p₁ p₃ p₂ = 0
-- Lean.Meta.SynthInstance
/-- Process the next subgoal in the given consumer node.  -/
Lean.Meta.SynthInstance.consume : Lean.Meta.SynthInstance.ConsumerNode → Lean.Meta.SynthInstance.SynthM Unit
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_2 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h