mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Instances.Real
IccRightChart_extend_top_mem_frontier : ∀ {x y : ℝ} [hxy : Fact (x < y)],
  ↑((IccRightChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊤ ∈
    frontier (Set.range ↑(modelWithCornersEuclideanHalfSpace 1))
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inl_comp_tensorHom : ∀ {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂),
  CategoryTheory.CategoryStruct.comp (x₁.inl x₂) (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) =
    CategoryTheory.CategoryStruct.comp f₁ (y₁.inl y₂)
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentations.mk.injEq : ∀ (presentations presentations_1 : Array ProofWidgets.ExprPresentationData),
  ({ presentations := presentations } = { presentations := presentations_1 }) = (presentations = presentations_1)
-- Mathlib.GroupTheory.Congruence.Hom
/-- The homomorphism on the quotient of an `AddMonoid` by an additive congruence
relation `c` induced by a homomorphism constant on `c`'s equivalence classes.  -/
AddCon.lift : {M : Type u_1} →
  {P : Type u_3} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass P] → (c : AddCon M) → (f : M →+ P) → c ≤ AddCon.ker f → c.Quotient →+ P
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- If `f` is almost everywhere positive, then `μ ≪ μ.withDensity f`. See also
`withDensity_absolutelyContinuous` for the reverse direction, which always holds.  -/
MeasureTheory.withDensity_absolutelyContinuous' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → (∀ᵐ (x : α) ∂μ, f x ≠ 0) → μ.AbsolutelyContinuous (μ.withDensity f)
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
/-- Make sure we can derive pullbacks in `Over B`.  -/
CategoryTheory.Over.instHasPullbacks : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Limits.HasPullbacks (CategoryTheory.Over B)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- Composition in the "underlying" category of an enriched category.  -/
CategoryTheory.ForgetEnrichment.homTo_comp : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] {X Y Z : CategoryTheory.ForgetEnrichment W C} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit W)).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.ForgetEnrichment.homTo W f)
          (CategoryTheory.ForgetEnrichment.homTo W g)))
      (CategoryTheory.eComp W (CategoryTheory.ForgetEnrichment.to W X) (CategoryTheory.ForgetEnrichment.to W Y)
        (CategoryTheory.ForgetEnrichment.to W Z))
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instDivisionMonoid : {α : Type u_1} → [DivisionMonoid α] → DivisionMonoid (Lex α)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.recv : {α : Type} → Std.CloseableChannel.Unbounded✝ α → BaseIO (Task (Option α))
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `lowerSemicontinuousAt_iff_frequently`. -/
LowerSemicontinuousAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α},
  LowerSemicontinuousAt f x → ∀ (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≤ y) → f x ≤ y
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_abs : ∀ {w i : ℕ} {x : BitVec w}, x.abs.getMsbD i = if x.msb = true then (-x).getMsbD i else x.getMsbD i
-- Mathlib.Data.List.Forall2
Relator.RightUnique.forall₂ : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, Relator.RightUnique R → Relator.RightUnique (List.Forall₂ R)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pullback of a `0`-hypercover along a morphism. The components are `pullback f (E.f i)`.  -/
CategoryTheory.Precoverage.ZeroHypercover.pullback₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S T : C} →
        [J.IsStableUnderBaseChange] →
          (f : S ⟶ T) →
            (E : J.ZeroHypercover T) → [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)] → J.ZeroHypercover S
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_Ioi_deriv_ofReal_cpow : ∀ {s : ℂ} {t : ℝ},
  0 < t → s.re < 0 → MeasureTheory.IntegrableOn (deriv fun x => ↑x ^ s) (Set.Ioi t) MeasureTheory.volume
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.inverse_range : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f : E →ₗ.[R] F}, f.toFun.ker = ⊥ → f.inverse.toFun.range = f.domain
-- Mathlib.Topology.Algebra.Support
tsupport_neg : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : SubtractionMonoid α] (f : X → α),
  tsupport (-f) = tsupport f
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Equivalence.prod_unitIso : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (E₁ : A ≌ B) (E₂ : C ≌ D),
  (E₁.prod E₂).unitIso = CategoryTheory.NatIso.prod E₁.unitIso E₂.unitIso
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a compact topological space, `α` a uniform space, and `F : ι → (X → α)` an
equicontinuous family. Then, the uniform structures of uniform convergence and pointwise
convergence induce the same uniform structure on `ι`.

In other words, pointwise convergence and uniform convergence coincide on an equicontinuous
subset of `X → α`.

This is a version of `Equicontinuous.comap_uniformFun_eq` stated in terms of `IsUniformInducing`
for convenience.  -/
Equicontinuous.isUniformInducing_uniformFun_iff_pi : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : UniformSpace ι] [CompactSpace X],
  Equicontinuous F → (IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_def : ∀ {u : ℕ → ENNReal}, ExpGrowth.expGrowthSup u = LinearGrowth.linearGrowthSup (ENNReal.log ∘ u)
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `Ioo a b` and
nonpositive on `Ioi b`. Then `f` attains its maximum on `Ioi a` at `b`.  -/
isMaxOn_Ioi_of_deriv : ∀ {f : ℝ → ℝ} {a b : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      DifferentiableOn ℝ f (Set.Ioi b) →
        (∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioi b, deriv f x ≤ 0) → IsMaxOn f (Set.Ioi a) b
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.eventually_right_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [inst_5 : CompleteSpace E] (hf : HasStrictFDerivAt f (↑f') a),
  ∀ᶠ (y : F) in nhds (f a), f (HasStrictFDerivAt.localInverse f f' a hf y) = y
-- Mathlib.MeasureTheory.Integral.Prod
/-- Change the order of integration for interval integrals.  -/
MeasureTheory.intervalIntegral_intervalIntegral_swap : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : ℝ → ℝ → E} {a b c d : ℝ},
  MeasureTheory.IntegrableOn (Function.uncurry F) (Set.uIoc a b ×ˢ Set.uIoc c d) MeasureTheory.volume →
    ∫ (x : ℝ) in a..b, ∫ (y : ℝ) in c..d, F x y = ∫ (y : ℝ) in c..d, ∫ (x : ℝ) in a..b, F x y
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.preservesSplitEqualizers : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.HasSplitEqualizer f g],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.Array.getElem?_zipWith.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (x : Option α) (x_1 : Option β)
  (h_1 : (a : α) → (b : β) → motive (some a) (some b)) (h_2 : (x : Option α) → (x_2 : Option β) → motive x x_2),
  (∀ (a : α) (b : β), x = some a → x_1 = some b → False) →
    (match x, x_1 with
      | some a, some b => h_1 a b
      | x, x_3 => h_2 x x_3) =
      h_2 x x_1
-- Batteries.Data.Array.Basic
/-- Folds a monadic function over an array from the left, accumulating the partial results starting with
`init`. The accumulated value is combined with the each element of the list in order, using `f`.

The optional parameters `start` and `stop` control the region of the array to be folded. Folding
proceeds from `start` (inclusive) to `stop` (exclusive), so no folding occurs unless `start < stop`.
By default, the entire array is folded.

Examples:
```lean example
example [Monad m] (f : α → β → m α) :
    Array.scanlM f x₀ #[a, b, c] = (do
      let x₁ ← f x₀ a
      let x₂ ← f x₁ b
      let x₃ ← f x₂ c
      pure #[x₀, x₁, x₂, x₃])
    := by simp [scanlM, scanlM.loop]
```

```lean example
example [Monad m] (f : α → β → m α) :
    Array.scanlM f x₀ #[a, b, c] (start := 1) (stop := 3) = (do
      let x₁ ← f x₀ b
      let x₂ ← f x₁ c
      pure #[x₀, x₁, x₂])
    := by simp [scanlM, scanlM.loop]
```
 -/
Array.scanlM : {m : Type u_1 → Type u_2} →
  {β : Type u_1} →
    {α : Type u_3} → [Monad m] → (β → α → m β) → β → (as : Array α) → optParam ℕ 0 → optParam ℕ as.size → m (Array β)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.inv_hom_apply : ∀ {R S : CommRingCat} (e : R ≅ S) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) r) = r
-- Init.Data.String.Termination
String.Slice.Pos.instWellFoundedRelation : {s : String.Slice} → WellFoundedRelation s.Pos
-- Mathlib.Probability.Kernel.CompProdEqIff
/-- A composition-product of a measure with a kernel defined with `withDensity` is equal to the
`withDensity` of the composition-product.  -/
MeasureTheory.Measure.compProd_withDensity : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} {f : α → β → ENNReal} [MeasureTheory.SFinite μ]
  [inst : ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel (κ.withDensity f)],
  Measurable (Function.uncurry f) → μ.compProd (κ.withDensity f) = (μ.compProd κ).withDensity fun p => f p.1 p.2
-- Mathlib.Algebra.Group.TypeTags.Finite
Fintype.card_additive : ∀ (α : Type u_1) [inst : Fintype α], Fintype.card (Additive α) = Fintype.card α
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.mk : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c ≤ c.ord.cof → c.IsRegular
-- Mathlib.Topology.Algebra.Group.Basic
Continuous.fun_zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous f → ∀ (z : ℤ), Continuous fun i => z • f i
-- Mathlib.GroupTheory.OrderOfElement
zsmul_smul_addOrderOf : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} {i : ℤ}, addOrderOf x • i • x = 0
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The global sections, notated Gamma.
 -/
AlgebraicGeometry.LocallyRingedSpace.Γ : CategoryTheory.Functor AlgebraicGeometry.LocallyRingedSpaceᵒᵖ CommRingCat
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousGeneratedBy.id : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y],
  Topology.ContinuousGeneratedBy X id
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- **Kummer's Theorem**

The `p`-adic valuation of `(n + k).choose k` is the number of carries when `k` and `n` are added
in base `p`. This sum is expressed over the finset `Ico 1 b` where `b` is any bound greater than
`log p (n + k)`.  -/
padicValNat_choose' : ∀ {p n k b : ℕ} [hp : Fact (Nat.Prime p)],
  Nat.log p (n + k) < b → padicValNat p ((n + k).choose k) = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card
-- Std.Internal.UV.UDP
/-- Sets the TTL value for outgoing packets.
 -/
Std.Internal.UV.UDP.Socket.setTTL : Std.Internal.UV.UDP.Socket → UInt32 → IO Unit
-- Mathlib.Topology.Algebra.InfiniteSum.Order
tprod_le_of_prod_le' : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α]
  [inst_2 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a₂ : α},
  1 ≤ a₂ → (∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂) → ∏'[L] (i : ι), f i ≤ a₂
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- `Matrix.toLin'` is a particular case of `Matrix.toLin`, for the standard basis
`Pi.basisFun R n`.  -/
Matrix.toLin_eq_toLin' : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n], Matrix.toLin (Pi.basisFun R n) (Pi.basisFun R m) = Matrix.toLin'
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.foldM.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (le : α → α → Bool)
  (s : Batteries.BinomialHeap.Imp.Heap α) (init : β) (f : β → α → m β),
  Batteries.BinomialHeap.Imp.Heap.foldM le s init f =
    match eq : Batteries.BinomialHeap.Imp.Heap.deleteMin le s with
    | none => pure init
    | some (hd, tl) =>
      have this := ⋯;
      do
      let __do_lift ← f init hd
      Batteries.BinomialHeap.Imp.Heap.foldM le tl __do_lift f
-- Mathlib.Order.Minimal
OrderIso.setOfPredMinimalIsoSetOfPredMaximal.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {t : Set β} (f : ↑s ≃o (↑t)ᵒᵈ),
  f.setOfPredMinimalIsoSetOfPredMaximal =
    { toFun := fun x => ⟨↑(f ⟨↑x, ⋯⟩), ⋯⟩, invFun := fun x => ⟨↑(f.symm ⟨↑x, ⋯⟩), ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_rel_iff' := ⋯ }
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M],
  ∃ n D d x,
    (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))
-- Mathlib.Topology.Maps.Basic
IsOpenMap.preimage_closure_subset_closure_preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {s : Set Y}, f ⁻¹' closure s ⊆ closure (f ⁻¹' s)
-- Mathlib.Order.Bounds.Basic
isGLB_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], IsGLB Set.univ ⊥
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.foldrM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (α → δ → m δ) → δ → Std.TreeSet.Raw α cmp → m δ
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {f : CategoryTheory.StructuredArrow S T},
  (CategoryTheory.StructuredArrow.map (CategoryTheory.CategoryStruct.id S)).obj f = f
-- Mathlib.FieldTheory.ChevalleyWarning
/-- The **Chevalley–Warning theorem**, binary version.
Let `f₁`, `f₂` be two multivariate polynomials in finitely many variables (`X s`, `s : σ`) over a
finite field of characteristic `p`.
Assume that the sum of the total degrees of `f₁` and `f₂` is less than the cardinality of `σ`.
Then the number of common solutions of the `f₁` and `f₂` is divisible by `p`.  -/
char_dvd_card_solutions_of_add_lt : ∀ {K : Type u_1} {σ : Type u_2} [inst : Fintype K] [inst_1 : Field K] [inst_2 : Fintype σ] [inst_3 : DecidableEq σ]
  [inst_4 : DecidableEq K] (p : ℕ) [CharP K p] {f₁ f₂ : MvPolynomial σ K},
  f₁.totalDegree + f₂.totalDegree < Fintype.card σ →
    p ∣ Fintype.card { x // (MvPolynomial.eval x) f₁ = 0 ∧ (MvPolynomial.eval x) f₂ = 0 }
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.iSup_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  (p : ι → Set M), ⨆ i, Submodule.span R (p i) = Submodule.span R (⋃ i, p i)
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_min : ∀ (m n : ℕ∞), ↑(min m n) = min ↑m ↑n
-- Mathlib.GroupTheory.Finiteness
Submonoid.FG.iSup : ∀ {M : Type u_1} [inst : Monoid M] {ι : Sort u_3} [Finite ι] (P : ι → Submonoid M), (∀ (i : ι), (P i).FG) → (iSup P).FG
-- Mathlib.Logic.Equiv.Defs
Equiv.leftInverse_symm : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.LeftInverse ⇑f.symm ⇑f
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_univ : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens}, X.zeroLocus Set.univ = (↑U)ᶜ
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.Kind.fromFile.sizeOf_spec : sizeOf Mathlib.Tactic.LibraryRewrite.Kind.fromFile = 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_insertIfNew_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β}, (m.insertIfNew k v).contains k = true
-- Mathlib.Algebra.Category.Grp.EpiMono
AddMonoidHom.range_eq_top_of_cancel : ∀ {A : Type u} {B : Type v} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] {f : A →+ B},
  (∀ (u v : B →+ B ⧸ f.range), u.comp f = v.comp f → u = v) → f.range = ⊤
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instIsCharPUInt64OfNatNat : Lean.Grind.IsCharP UInt64 18446744073709551616
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanStaleDependencyParams.mk.injEq : ∀ (staleDependency staleDependency_1 : Lean.Lsp.DocumentUri),
  ({ staleDependency := staleDependency } = { staleDependency := staleDependency_1 }) =
    (staleDependency = staleDependency_1)
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.State.isMeta : Lean.ParseImports.State → Bool
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.eq_zero_of_add_left : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] [IsFormallyReal R] {s₁ s₂ : R},
  IsSumSq s₁ → IsSumSq s₂ → s₁ + s₂ = 0 → s₂ = 0
-- Mathlib.GroupTheory.Divisible
RootableBy.surjective_pow : ∀ (A : Type u_1) (α : Type u_2) [inst : Monoid A] [inst_1 : Pow A α] [inst_2 : Zero α] [RootableBy A α] {n : α},
  n ≠ 0 → Function.Surjective fun a => a ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (MvPolynomial.eval P) W.polynomialX / P 2 ^ 2 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomialX
-- Mathlib.Algebra.Lie.Weights.Chain
/-- Given two (potential) weights `χ₁` and `χ₂` together with integers `p` and `q`, it is often
useful to study the sum of weight spaces associated to the family of weights `k • χ₁ + χ₂` for
`p < k < q`.  -/
LieModule.genWeightSpaceChain : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [LieModule R L M] → [LieRing.IsNilpotent L] → (L → R) → (L → R) → ℤ → ℤ → LieSubmodule R L M
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.id_mapComp_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.StrictPseudofunctor.id B).mapComp f g).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Tactic.Sat.FromLRAT
/-- The empty clause  -/
Sat.Clause.nil : Sat.Clause
-- Mathlib.Order.SuccPred.Basic
/-- The successor of an element. If `a` is not maximal, then `succ a` is the least element greater
than `a`. If `a` is maximal, then `succ a = a`.  -/
Order.succ : {α : Type u_1} → [inst : Preorder α] → [SuccOrder α] → α → α
-- Mathlib.AlgebraicTopology.SimplicialSet.Subdivision
SSet.instIsRightAdjointEx : SSet.ex.IsRightAdjoint
-- Mathlib.Algebra.Ring.BooleanRing
BoundedLatticeHom.asBoolRing_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  [inst_2 : BooleanAlgebra γ] (g : BoundedLatticeHom β γ) (f : BoundedLatticeHom α β),
  (g.comp f).asBoolRing = g.asBoolRing.comp f.asBoolRing
-- Std.Http.Protocol.H1.Config
/-- Maximum length of header field name (default: 256 bytes).
 -/
Std.Http.Protocol.H1.Config.maxHeaderNameLength : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Data.Multiset.Bind
Multiset.dedup_bind_dedup : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (s : Multiset α) (f : α → Multiset β),
  (s.dedup.bind f).dedup = (s.bind f).dedup
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.basis.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R),
  WeierstrassCurve.Affine.CoordinateRing.basis W' =
    ⋯.by_cases (fun x => default) fun x => (AdjoinRoot.powerBasis' ⋯).basis.reindex (finCongr ⋯)
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.measurable_of_measurable_coe : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : β → MeasureTheory.Measure α),
  (∀ (s : Set α), MeasurableSet s → Measurable fun b => (f b) s) → Measurable f
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.evalConstCore : (α : Type u_1) → Lean.Environment → Lean.Options → Lean.Name → Except String α
-- Mathlib.Order.Compare
cmp_eq_gt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] (x y : α), cmp x y = Ordering.gt ↔ y < x
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.continuous_integral : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E], Continuous fun f => MeasureTheory.L1.integral f
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- Helper structure for the construction of a term in `SmallCategoryOfSet`.
This involves the choice of bijections between types of objects and morphisms
in a category `C` and subtypes of a type `Ω`.  -/
CategoryTheory.CoreSmallCategoryOfSet : Type w → (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max (max u v) w)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.image_β_hom : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), (S.unionProd T).image (β_ X Y).hom = T.unionProd S
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finsums of meromorphic functions are meromorphic.  -/
MeromorphicAt.finsum : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {ι : Type u_5} {F : ι → 𝕜 → 𝕜'} {x : 𝕜},
  (∀ (i : ι), MeromorphicAt (F i) x) → MeromorphicAt (∑ᶠ (i : ι), F i) x
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_map_of_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β},
  Function.Injective f → ∀ (s : Multiset α), (Multiset.map f s).dedup = Multiset.map f s.dedup
-- Mathlib.Order.IsNormal
Order.IsNormal.monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Order.IsNormal f → Monotone f