mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestRevMatchAtChain_of_ofSliceFrom : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {startPos endPos : (s.sliceFrom p).Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat (String.Slice.Pos.ofSliceFrom startPos)
      (String.Slice.Pos.ofSliceFrom endPos) →
    String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat startPos endPos
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.map_roots_le_of_injective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  (p : Polynomial A) {f : A →+* B}, Function.Injective ⇑f → Multiset.map (⇑f) p.roots ≤ (Polynomial.map f p).roots
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.zero_add : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (0 + a) a
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.continuous_extend : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  {f : α → β} [CompleteSpace β], Continuous (pkg.extend f)
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.mk.sizeOf_spec : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' : Φ.LeftResolution X₂} [inst_2 : SizeOf C₁] [inst_3 : SizeOf C₂]
  [inst_4 : ⦃X Y : C₁⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)] [inst_5 : ⦃X Y : C₂⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)]
  (f : L.X₁ ⟶ L'.X₁)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp (Φ.functor.map f) L'.w = L.w)
      CategoryTheory.LocalizerMorphism.LeftResolution.Hom.comm._autoParam),
  sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_eq_false_of_isEmpty_erase_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → t.isEmpty = false
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.stacksTagParser.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Order.Lemmas
Std.min_le_right : ∀ {α : Type u} [inst : Min α] [inst_1 : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2] [Std.LawfulOrderInf α] {a b : α},
  a ⊓ b ≤ b
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.dot_neg_left : ∀ (xs ys : Lean.Omega.IntList), Lean.Omega.Coeffs.dot (-xs) ys = -Lean.Omega.Coeffs.dot xs ys
-- Mathlib.Data.ENat.Basic
ENat.one_le_iff_ne_zero : ∀ {n : ℕ∞}, 1 ≤ n ↔ n ≠ 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.inclusion_refl : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  CategoryTheory.Subgroupoid.inclusion ⋯ = CategoryTheory.Functor.id ↑S.objs
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom_unique : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  (J : Ideal P) [inst_2 : J.IsPrime] (f : R →+* P) (hIJ : I = Ideal.comap f J)
  {j : Localization.AtPrime I →+* Localization.AtPrime J},
  (∀ (x : R), j ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)) →
    Localization.localRingHom I J f hIJ = j
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.det_submatrix_removeNth_eq_sign_mul_bminor : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} (α : Fin (p + 1) → Fin n)
  (i : Fin n) (s : Fin (p + 1)),
  (A.submatrix (Fin.cons i (s.removeNth α)) α).det = (-1) ^ ↑s * BirdDet.bminor✝ A i (α s) (s.removeNth α)
-- Std.Time.Date.Unit.Day
/-- Converts an `OfYear` ordinal to a `Offset`.
 -/
Std.Time.Day.Ordinal.OfYear.toOffset : {leap : Bool} → Std.Time.Day.Ordinal.OfYear leap → Std.Time.Day.Offset
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainGoalParams : Lean.ToJson Lean.Lsp.PlainGoalParams
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
/-- A square matrix `A` over a commutative semiring `R` is "determinant balanced"
with respect to `a b : R` if `a|A|⁺ + b|A|⁻ = b|A|⁺ + a|A|⁻`. Over a commutative ring,
this is equivalent to `(a - b)|A| = 0`, see `Matrix.isDetpBalanced_iff_sub_mul_det_eq_zero`.  -/
Matrix.IsDetpBalanced : {n : Type u_1} → {R : Type u_3} → [Fintype n] → [DecidableEq n] → [CommSemiring R] → Matrix n n R → R → R → Prop
-- Init.Grind.ToInt
/-- The finite interval `[lo, hi)`.  -/
Lean.Grind.IntInterval.co : ℤ → ℤ → Lean.Grind.IntInterval
-- Mathlib.Data.Finset.Sups
Finset.biUnion_image_sup_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] (s t : Finset α),
  (t.biUnion fun b => Finset.image (fun x => x ⊔ b) s) = s ⊻ t
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNeg_eq_neg : ∀ {M : Type u_1} [inst : AddGroup M] (S : AddSubmonoid M), S.leftNeg = -S
-- Mathlib.LinearAlgebra.RootSystem.Reduced
/-- See also `RootPairing.pairingIn_two_two_iff`.  -/
RootPairing.pairing_two_two_iff : ∀ {ι : 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) (i j : ι) [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M], P.pairing i j = 2 ∧ P.pairing j i = 2 ↔ i = j
-- Mathlib.Algebra.GCDMonoid.PUnit
PUnit.norm_unit_eq : ∀ {x : PUnit.{u_1 + 1}}, normUnit x = 1
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Two points are collinear.  -/
collinear_pair : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (p₁ p₂ : P), Collinear k {p₁, p₂}
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.copy_dropPrefix?_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice},
  Option.map String.Slice.copy (s.copy.dropPrefix? pat) = Option.map String.Slice.copy (s.dropPrefix? pat)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α}, m.getKey? k = some k' → k' ∈ m
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.forget₂_obj : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Y : TopCat),
  CategoryTheory.HasForget₂.forget₂.obj Y = { carrier := ↑Y, str := Y.str }
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_or : ∀ (x y i : ℕ), (x ||| y).testBit i = (x.testBit i || y.testBit i)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_iSup_of_directed : ∀ {R : Type u} [inst : NonAssocRing R] {ι : Sort u_1} [hι : Nonempty ι] {S : ι → Subring R},
  Directed (fun x1 x2 => x1 ≤ x2) S → ↑(⨆ i, S i) = ⋃ i, ↑(S i)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (e : T ≅ T')
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₃ = e.inv.hom₃
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.notMem_neLocus : ∀ {α : Type u_1} {N : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq N] [inst_2 : Zero N] {f g : α →₀ N}
  {a : α}, a ∉ f.neLocus g ↔ f a = g a
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f` is meromorphic of finite order at `x`, then the trailing coefficient is not zero.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → meromorphicOrderAt f x ≠ ⊤ → meromorphicTrailingCoeffAt f x ≠ 0
-- Mathlib.Order.CompleteLattice.Finset
Finset.subset_set_biUnion_of_mem : ∀ {α : Type u_2} {β : Type u_3} {s : Finset α} {f : α → Set β} {x : α}, x ∈ s → f x ⊆ ⋃ y ∈ s, f y
-- Mathlib.Geometry.Euclidean.Volume.Measure
Isometry.map_euclideanHausdorffMeasure : ∀ {X : Type u_1} {Y : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X]
  [inst_3 : EMetricSpace Y] [inst_4 : MeasurableSpace Y] [inst_5 : BorelSpace Y] {f : X → Y} {d : ℕ},
  Isometry f →
    MeasureTheory.Measure.map f (MeasureTheory.Measure.euclideanHausdorffMeasure d) =
      (MeasureTheory.Measure.euclideanHausdorffMeasure d).restrict (Set.range f)
-- Mathlib.Probability.StrongLaw
/-- **Strong law of large numbers**, almost sure version: if `X n` is a sequence of independent
identically distributed integrable real-valued random variables, then `∑ i ∈ range n, X i / n`
converges almost surely to `𝔼[X 0]`. We give here the strong version, due to Etemadi, that only
requires pairwise independence. Superseded by `strong_law_ae`, which works for random variables
taking values in any Banach space.  -/
ProbabilityTheory.strong_law_ae_real : ∀ {Ω : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) μ →
    Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
        ∀ᵐ (ω : Ω) ∂μ,
          Filter.Tendsto (fun n => (∑ i ∈ Finset.range n, X i ω) / ↑n) Filter.atTop (nhds (∫ (x : Ω), X 0 x ∂μ))
-- Mathlib.Data.Set.Function
Set.InjOn.image_subset_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s s₁ s₂ : Set α} {f : α → β},
  Set.InjOn f s → s₁ ⊆ s → s₂ ⊆ s → (f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂)
-- Mathlib.Data.List.OfFn
List.ofFn_get : ∀ {α : Type u} (l : List α), List.ofFn l.get = l
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Mathlib.Logic.Equiv.Defs
EquivLike.apply_coe_symm_apply : ∀ {α : Sort u} {β : Sort v} {F : Sort u_1} [inst : EquivLike F α β] (e : F) (x : β), e ((↑e).symm x) = x
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.cases.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {cases cases_1 : Lean.Compiler.LCNF.Cases pu},
  Lean.Compiler.LCNF.Code.cases cases = Lean.Compiler.LCNF.Code.cases cases_1 → cases = cases_1
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.toAddSubgroup_ofAddSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [inst_1 : H.Normal] [inst_2 : H.FiniteIndex],
  (FiniteIndexNormalAddSubgroup.ofAddSubgroup H).toAddSubgroup = H
-- Lean.ResolveName
Lean.ResolveName.resolveNamespaceUsingScope? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.not_equiv_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 1 * Q 2 ^ 3 ≠ Q 1 * P 2 ^ 3 → ¬P ≈ Q
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Biproduct.column_nonzero_of_iso' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {σ τ : Type} [Finite τ]
  {S : σ → C} [inst_3 : CategoryTheory.Limits.HasBiproduct S] {T : τ → C}
  [inst_4 : CategoryTheory.Limits.HasBiproduct T] (s : σ) (f : ⨁ S ⟶ ⨁ T) [CategoryTheory.IsIso f],
  (∀ (t : τ),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι S s)
          (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.biproduct.π T t)) =
        0) →
    CategoryTheory.CategoryStruct.id (S s) = 0
-- Mathlib.RingTheory.AdjoinRoot
/-- The canonical algebraic equivalence between `AdjoinRoot f` and `AdjoinRoot g`, where
the two polynomials `f g : S[X]` are equal.  -/
AdjoinRoot.algEquivOfEq : (R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (f g : Polynomial S) → f = g → AdjoinRoot f ≃ₐ[R] AdjoinRoot g
-- Mathlib.Data.Finset.Card
Finset.injOn_of_card_image_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α → β} [inst : DecidableEq β],
  (Finset.image f s).card = s.card → Set.InjOn f ↑s
-- Mathlib.Algebra.Group.Defs
Semigroup.toMul : {G : Type u} → [self : Semigroup G] → Mul G
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_transpose_mul_self : ∀ {α : Type u_1} {n : Type u_3} [inst : Fintype n] [inst_1 : NonUnitalCommSemiring α] (A : Matrix n n α),
  (A.transpose * A).IsSymm
-- Mathlib.Order.CountableSupClosed
countableSupClosure_idem : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), countableSupClosure (countableSupClosure s) = countableSupClosure s
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabPanic : Lean.Elab.Term.TermElab
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `atBot` and `g` tends to `C` then `f + g` tends to `atBot`.  -/
Filter.Tendsto.atBot_add : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the 1-dimensional derivative.

Version for a Schwartz function with values in continuous linear maps.  -/
SchwartzMap.integral_smul_deriv_right_eq_neg_left : ∀ {𝕜 : Type u_2} {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [inst_2 : RCLike 𝕜]
  [inst_3 : NormedSpace 𝕜 F] (f : SchwartzMap ℝ 𝕜) (g : SchwartzMap ℝ F),
  ∫ (x : ℝ), f x • deriv (⇑g) x = -∫ (x : ℝ), deriv (⇑f) x • g x
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The endomorphism monoid of a root pairing.  -/
RootPairing.End : {ι : 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] → RootPairing ι R M N → Type (max (max (max (max (max u_1 u_3) u_4) u_1) u_3) u_4)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv.eq_1 : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T),
  hST.equiv = (Equiv.ofBijective (fun x => ↑x.1 * ↑x.2) hST).symm
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.willSave : Lean.Lsp.TextDocumentSyncOptions → Bool
-- Mathlib.Data.Int.Init
Int.dvd_div_iff_mul_dvd : ∀ {a b c : ℤ}, c ∣ b → (a ∣ b / c ↔ c * a ∣ b)
-- Init.Data.Sum.Lemmas
Sum.eq_right_getRight_of_isRight : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β} (h : x.isRight = true), x = Sum.inr (x.getRight h)
-- Lean.Util.SCC
Lean.SCC.Data.index? : Lean.SCC.Data → Option ℕ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool} {k k' : α} {fallback : β},
  m.getKey? k = some k' →
    (Std.HashMap.filter f m).getD k fallback = (Option.filter (fun x => f k' x) m[k]?).getD fallback
-- Mathlib.Analysis.Analytic.Basic
analyticAt_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  f =ᶠ[nhds x] g → (AnalyticAt 𝕜 f x ↔ AnalyticAt 𝕜 g x)
-- Init.Data.Array.QSort.Basic
/-- In-place quicksort.

`qsort as lt lo hi` sorts the subarray `as[lo...=hi]` in-place using `lt` to compare elements.
 -/
Array.qsort : {α : Type u_1} →
  (as : Array α) → autoParam (α → α → Bool) Array.qsort._auto_1 → optParam ℕ 0 → optParam ℕ (as.size - 1) → Array α
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.vertices_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E}, K.vertices = ⋃ k ∈ K.faces, ↑k
-- Mathlib.RingTheory.FreeCommRing
/-- The free ring on a type with one term is isomorphic to `ℤ[X]`.  -/
freeRingPUnitEquivPolynomialInt : FreeRing PUnit.{u + 1} ≃+* Polynomial ℤ
-- Init.Data.Array.Find
Array.find?_push : ∀ {α : Type u_1} {a : α} {p : α → Bool} {xs : Array α},
  Array.find? p (xs.push a) = (Array.find? p xs).or (if p a = true then some a else none)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.instHasColimitsOfShape : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.CosimplicialObject C)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.instCategory : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  CategoryTheory.Category.{max (max u_2 v_1) v_2, max (max (max u_2 v_2) u_1) v_1}
                    (CategoryTheory.Triangulated.SpectralObject C ι)
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- Inherit `FunLike` structure from `C(X, R) →L[R] E`.  -/
AbstractMeasure.instFunLikeContinuousMap : {X : Type u_1} →
  {R : Type u_3} →
    {E : Type u_4} →
      [inst : TopologicalSpace X] →
        [inst_1 : AddCommGroup E] →
          [inst_2 : TopologicalSpace E] →
            [inst_3 : CommRing R] →
              [inst_4 : TopologicalSpace R] →
                [inst_5 : IsTopologicalRing R] → [inst_6 : Module R E] → FunLike (AbstractMeasure X R E) C(X, R) E
-- Lean.Environment
/-- Stores each given module data in the respective file name. Objects shared with prior parts are not
duplicated. Thus the data cannot be loaded with individual `readModuleData` calls but must loaded by
passing (a prefix of) the file names to `readModuleDataParts`. `mod` is used to determine an
arbitrary but deterministic base address for `mmap`.
 -/
Lean.saveModuleDataParts : Lean.Name → Array (System.FilePath × Lean.ModuleData) → IO Unit
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Ioc : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc '' Set.Ioc i j = Set.Ioc i.castSucc j.castSucc
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleAlgebra.toSMulCommClass : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieAdmissibleRing L} [self : LieAdmissibleAlgebra R L],
  SMulCommClass R L L
-- Lean.Parser.Term
/-- A resolved name literal. Evaluates to the full name of the given constant if
existent in the current context, or else fails.
 -/
Lean.Parser.Term.doubleQuotedName : Lean.Parser.Parser
-- Mathlib.Topology.Instances.Matrix
instTopologicalSpaceMatrix : {m : Type u_4} → {n : Type u_5} → {R : Type u_8} → [TopologicalSpace R] → TopologicalSpace (Matrix m n R)
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.LawfulMapOperator.denote_prefix_cast_ref : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input1 input2 : aig.Ref} {f : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α}
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f]
  {h : aig.decls.size ≤ (f aig input1).aig.decls.size},
  ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧
-- Mathlib.Data.Nat.Factorization.Defs
Nat.dvd_prod_pow_of_factorization_le : ∀ {n : ℕ} {f : ℕ →₀ ℕ}, n ≠ 0 → n.factorization ≤ f → n ∣ f.prod fun x1 x2 => x1 ^ x2
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An affine combination, over the image of an embedding, equals an
affine combination with the same points and weights over the original
`Finset`.  -/
Finset.affineCombination_map : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} {ι₂ : Type u_5} (s₂ : Finset ι₂) (e : ι₂ ↪ ι) (w : ι → k) (p : ι → P),
  (Finset.affineCombination k (Finset.map e s₂) p) w = (Finset.affineCombination k s₂ (p ∘ ⇑e)) (w ∘ ⇑e)
-- Mathlib.Topology.GDelta.Basic
/-- A countable intersection of Gδ sets is a Gδ set.  -/
IsGδ.sInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)}, (∀ s ∈ S, IsGδ s) → S.Countable → IsGδ (⋂₀ S)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.mem_sInf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (s : Set (CategoryTheory.GrothendieckTopology C)) {X : C}
  (S : CategoryTheory.Sieve X), S ∈ (sInf s) X ↔ ∀ t ∈ s, S ∈ t X
-- Mathlib.Logic.Equiv.Defs
Equiv.sumIsRight_symm_apply_coe : ∀ {α : Type u_1} {β : Type u_2} (b : β), ↑(Equiv.sumIsRight.symm b) = Sum.inr b
-- Mathlib.Computability.EpsilonNFA
εNFA.isPath_iff : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) (a a_1 : σ) (a_2 : List (Option α)),
  M.IsPath a a_1 a_2 ↔ a_1 = a ∧ a_2 = [] ∨ ∃ t a_3 x, t ∈ M.step a a_3 ∧ M.IsPath t a_1 x ∧ a_2 = a_3 :: x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapComp : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.id B).mapComp f g =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
/-- A family of elements indexed by `Sieve.ofObjects Y X` that is induced by
`x : FamilyOfElementsOnObjects F Y`. See the equational lemma
`IsCompatible.familyOfElements_apply` which holds under the assumption `x.IsCompatible`.  -/
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.familyOfElements : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {I : Type u_1} →
        {Y : I → C} →
          CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y →
            (X : C) → CategoryTheory.Presieve.FamilyOfElements F (CategoryTheory.Sieve.ofObjects Y X).arrows
-- Mathlib.GroupTheory.OrderOfElement
/-- An additive equivalence preserves orders of elements.  -/
AddEquiv.addOrderOf_eq : ∀ {G : Type u_1} [inst : AddMonoid G] {H : Type u_6} [inst_1 : AddMonoid H] (e : G ≃+ H) (x : G),
  addOrderOf (e x) = addOrderOf x
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_of_le_smul : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ μ' : MeasureTheory.Measure α} {c : ENNReal},
  μ' ≤ c • μ → μ'.AbsolutelyContinuous μ
-- Init.Data.Format.Basic
/-- Used for associating auxiliary information (e.g. `Expr`s) with `Format` objects.  -/
Std.Format.tag : ℕ → Std.Format → Std.Format