mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.C1.congr_simp : ∀ {I : Type u} (C C_1 : Set (I → Bool)),
  C = C_1 →
    ∀ [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o o_1 : Ordinal.{u}} (e_o : o = o_1)
      (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (a a_1 : I → Bool),
      a = a_1 → Profinite.NobelingProof.C1 C ho a = Profinite.NobelingProof.C1 C_1 ⋯ a_1
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic_prime_mul_X_sub_one : ∀ (R : Type u_1) [inst : Ring R] (p : ℕ) [hn : Fact (Nat.Prime p)],
  Polynomial.cyclotomic p R * (Polynomial.X - 1) = Polynomial.X ^ p - 1
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `L / K` be a normal field extension. For any two elements `x` and `y` in `L`, `y` is a
conjugate root of `x` if and only if there exists a `K`-automorphism `σ : Gal(L/K)` such
that `σ y = x`.
 -/
isConjRoot_iff_exists_algEquiv : ∀ {K : Type u_2} {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Normal K L] {x y : L},
  IsConjRoot K x y ↔ ∃ σ, σ y = x
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.opensHom.instFunLike : {X : TopCat} → {U V : TopologicalSpace.Opens ↑X} → FunLike (U ⟶ V) ↥U ↥V
-- Init.Data.Vector.Lemmas
Vector.toList_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n},
  (Vector.zipWith f as bs).toList = List.zipWith f as.toList bs.toList
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- A family of vectors is linearly independent if they are nonzero
and orthogonal.  -/
linearIndependent_of_ne_zero_of_inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  (∀ (i : ι), v i ≠ 0) → (Pairwise fun i j => inner 𝕜 (v i) (v j) = 0) → LinearIndependent 𝕜 v
-- Qq.Simp
/-- Build a simproc with Qq-enabled typechecking of inputs and outputs.

This calls `inferTypeQ` on the expression and passes the arguments to `proc`.  -/
Lean.Meta.Simp.Simproc.ofQ : Lean.Meta.Simp.SimprocQ → Lean.Meta.Simp.Simproc
-- Mathlib.Data.Finset.Defs
Finset.val_lt_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁.val < s₂.val ↔ s₁ ⊂ s₂
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toAddSubgroup_top : ∀ {R : Type u} [inst : NonAssocRing R], ⊤.toAddSubgroup = ⊤
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, (m.erase k).getKeyD k fallback = fallback
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated additive submonoids is finitely generated.  -/
AddSubmonoid.FG.pi : ∀ {ι : Type u_3} [Finite ι] {M : ι → Type u_4} [inst : (i : ι) → AddMonoid (M i)] {P : (i : ι) → AddSubmonoid (M i)},
  (∀ (i : ι), (P i).FG) → (AddSubmonoid.pi Set.univ P).FG
-- Lean.Data.Lsp.Basic
Lean.Lsp.instHashableMarkupKind : Hashable Lean.Lsp.MarkupKind
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The Ore subtrahend of a difference.  -/
AddOreLocalization.oreSubtra : {R : Type u_1} → [inst : AddMonoid R] → {S : AddSubmonoid R} → [AddOreLocalization.AddOreSet S] → R → ↥S → ↥S
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.inter_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ m₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → ∀ (h₃ : m₃.WF), m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁.inter m₂ ⋯).Equiv (m₃.inter m₄ ⋯)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (n : ℕ), (Polynomial.C r * Polynomial.X ^ n).eraseLead = 0
-- Mathlib.Algebra.Order.Group.PosPart
Pi.leOnePart_def : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Lattice (α i)] [inst_1 : (i : ι) → Group (α i)]
  (f : (i : ι) → α i), f⁻ᵐ = fun i => (f i)⁻ᵐ
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.trans_of_left_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v w : V} (hv : f v = 0) (hw : f w = 0)
  (hvw : autoParam (f (v + w) = 0) LinearEquiv.transvection.trans_of_left_eq._auto_1),
  LinearEquiv.transvection hw ≪≫ₗ LinearEquiv.transvection hv = LinearEquiv.transvection hvw
-- Init.Data.SInt.Bitwise
Int32.not_eq_neg_add : ∀ (a : Int32), ~~~a = -a - 1
-- Init.Data.SInt.Lemmas
Int32.ofBitVec_int64ToBitVec : ∀ (x : Int64), Int32.ofBitVec (BitVec.signExtend 32 x.toBitVec) = x.toInt32
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
AffineIsometry.angle_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] (f : P →ᵃⁱ[ℝ] P₂)
  (p₁ p₂ p₃ : P), EuclideanGeometry.angle (f p₁) (f p₂) (f p₃) = EuclideanGeometry.angle p₁ p₂ p₃
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_one : ∀ (S : Type u) [inst : Semiring S], ascPochhammer S 1 = Polynomial.X
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Restricting a chart of `M` to an open subset `s` yields a chart in the maximal atlas of `s`.

NB. We cannot deduce membership in `atlas H s` in general: by definition, this atlas contains
precisely the restriction of each preferred chart at `x ∈ s` --- whereas `atlas H M`
can contain more charts than these.  -/
StructureGroupoid.subtypeRestr_mem_maximalAtlas : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {e : OpenPartialHomeomorph M H},
  e ∈ atlas H M →
    ∀ {s : TopologicalSpace.Opens M} (hs : Nonempty ↥s) {G : StructureGroupoid H} [HasGroupoid M G]
      [ClosedUnderRestriction G], e.subtypeRestr hs ∈ StructureGroupoid.maximalAtlas (↥s) G
-- Init.Data.SInt.Lemmas
ISize.toBitVec_add : ∀ {a b : ISize}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.ellipsis : Lean.Elab.Term.CollectPatternVars.Context → Bool
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)],
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit
          (CategoryTheory.MonoidalCategory.DayFunctor C V)).functor.IsLeftKanExtension
    (CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans C V)
-- Init.Data.UInt.Basic
/-- Bitwise exclusive or for 8-bit unsigned integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.xor : UInt8 → UInt8 → UInt8
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- `Set α` is a commutative subtraction monoid under pointwise operations if `α` is.  -/
Set.subtractionCommMonoid : {α : Type u_2} → [SubtractionCommMonoid α] → SubtractionCommMonoid (Set α)
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- Up to isomorphism an element of the fiber of `X` only lies in one connected component.  -/
CategoryTheory.PreGaloisCategory.connected_component_unique : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A B : C}
  [CategoryTheory.PreGaloisCategory.IsConnected A] [CategoryTheory.PreGaloisCategory.IsConnected B] (a : (F.obj A).obj)
  (b : (F.obj B).obj) (i : A ⟶ X) (j : B ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.map i)) a = (CategoryTheory.ConcreteCategory.hom (F.map j)) b →
    ∀ [CategoryTheory.Mono i] [CategoryTheory.Mono j], ∃ f, (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a = b
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.eventually_filterAt_measurableSet : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) (x : X), ∀ᶠ (t : Set X) in v.filterAt x, MeasurableSet t
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.volume_preserving_prodAssoc : ∀ {α₁ : Type u_4} {β₁ : Type u_5} {γ₁ : Type u_6} [inst : MeasureTheory.MeasureSpace α₁]
  [inst_1 : MeasureTheory.MeasureSpace β₁] [inst_2 : MeasureTheory.MeasureSpace γ₁]
  [MeasureTheory.SFinite MeasureTheory.volume] [MeasureTheory.SFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑MeasurableEquiv.prodAssoc) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.CategoryTheory.Sites.LocallySurjective
/-- The image of `F` in `J.sheafify F` is isomorphic to the sheafification.  -/
CategoryTheory.Presheaf.sheafificationIsoImagePresheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))) →
        J.sheafify F ≅
          (CategoryTheory.Subfunctor.sheafify J (CategoryTheory.Subfunctor.range (J.toSheafify F))).toFunctor
-- Mathlib.Order.BoundedOrder.Basic
top_eq_true : ⊤ = true
-- Lean.Setup
/-- Pre-resolved artifacts of transitively imported modules.  -/
Lean.ModuleSetup.importArts : Lean.ModuleSetup → Lean.NameMap Lean.ImportArtifacts
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restrict the domain and codomain of an `AddMonoidHom`.  -/
AddMonoidHom.restrict : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {M' : AddSubmonoid M} → {N' : AddSubmonoid N} → {f : M →+ N} → Set.MapsTo ⇑f ↑M' ↑N' → ↥M' →+ ↥N'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_le_size_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α}, m.size ≤ (Std.DHashMap.Const.insertManyIfNewUnit m l).size
-- Init.Data.Fin.Lemmas
Fin.lt_trans : ∀ {n : ℕ} {a b c : Fin n}, a < b → b < c → a < c
-- Aesop.Forward.State
Aesop.instHashableRawHyp : Hashable Aesop.RawHyp
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_le_iff_le_functorPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (S : CategoryTheory.Sieve X) (R : CategoryTheory.Sieve (F.obj X)),
  CategoryTheory.Sieve.functorPushforward F S ≤ R ↔ S ≤ CategoryTheory.Sieve.functorPullback F R
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_neg : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), ⇑(-f) = -⇑f
-- Mathlib.LinearAlgebra.Basis.Basic
/-- A linear independent family of vectors spanning the whole module is a basis.  -/
Module.Basis.mk : {ι : Type u_1} →
  {R : Type u_3} →
    {M : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            {v : ι → M} → LinearIndependent R v → ⊤ ≤ Submodule.span R (Set.range v) → Module.Basis ι R M
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Auxiliary type for normalizing `Ring` and `Field` disequalities.  -/
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr : Type
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.ext_iff : ∀ {ι : Type u_1} {x y : PreAbstractSimplicialComplex ι}, x = y ↔ x.faces = y.faces
-- Mathlib.Data.Set.Image
Set.image_of_range_union_range_eq_univ : ∀ {α : Type u_5} {β : Type u_6} {γ : Type u_7} {γ' : Type u_8} {δ : Type u_9} {δ' : Type u_10} {h : β → α} {f : γ → β}
  {f₁ : γ' → α} {f₂ : γ → γ'} {g : δ → β} {g₁ : δ' → α} {g₂ : δ → δ'},
  h ∘ f = f₁ ∘ f₂ →
    h ∘ g = g₁ ∘ g₂ →
      Set.range f ∪ Set.range g = Set.univ → ∀ (s : Set β), h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isOpenEmbedding_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U →
    Continuous f → (Topology.IsOpenEmbedding f ↔ ∀ (i : ι), Topology.IsOpenEmbedding ((U i).carrier.restrictPreimage f))
-- Lean.Message
Lean.MessageSeverity.information.sizeOf_spec : sizeOf Lean.MessageSeverity.information = 1
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_mul_right_closedBall : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ℝ),
  (fun x => x * a) ⁻¹' Metric.closedBall b r = Metric.closedBall (b / a) r
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- Note that this should not be used directly, and `eq_moduleTopology`, which takes `R` and `A`
explicitly, should be used instead.  -/
IsModuleTopology.eq_moduleTopology' : ∀ {R : Type u_1} {inst : TopologicalSpace R} {A : Type u_2} {inst_1 : Add A} {inst_2 : SMul R A}
  {τA : TopologicalSpace A} [self : IsModuleTopology R A], τA = moduleTopology R A
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.mk.injEq : ∀ {α : Type u_5} {β : Type u_6} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (toMulHom : α →ₙ* β) (map_zero' : toMulHom.toFun 0 = 0)
  (map_add' : ∀ (x y : α), toMulHom.toFun (x + y) = toMulHom.toFun x + toMulHom.toFun y) (toMulHom_1 : α →ₙ* β)
  (map_zero'_1 : toMulHom_1.toFun 0 = 0)
  (map_add'_1 : ∀ (x y : α), toMulHom_1.toFun (x + y) = toMulHom_1.toFun x + toMulHom_1.toFun y),
  ({ toMulHom := toMulHom, map_zero' := map_zero', map_add' := map_add' } =
      { toMulHom := toMulHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 }) =
    (toMulHom = toMulHom_1)
-- Mathlib.NumberTheory.NumberField.House
NumberField.norm_embedding_le_house : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (α : K) (σ : K →+* ℂ), ‖σ α‖ ≤ NumberField.house α
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_smul : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : SMul α β] (s : ι → Set α) (t : Set β),
  (⋃ i, s i) • t = ⋃ i, s i • t
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_apply_dite : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [inst : CommMonoid M] {p : ι → Prop}
  [inst_1 : DecidablePred p] [inst_2 : DecidablePred fun x => ¬p x] (f : (x : ι) → p x → γ) (g : (x : ι) → ¬p x → γ)
  (h : γ → M), ∏ x ∈ s, h (if hx : p x then f x hx else g x hx) = (∏ x, h (f ↑x ⋯)) * ∏ x, h (g ↑x ⋯)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_one : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A}, HomogeneousLocalization.val 1 = 1
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance : (pat : String.Slice) →
  UInt8 →
    (table : Array ℕ) →
      table.size ≤ pat.utf8ByteSize →
        (∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) → (guess : ℕ) → guess < table.size → { n // n ≤ table.size }
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : SupSet α] → [inst_1 : SupSet β] → FunLike (sSupHom α β) α β
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, Std.DTreeMap.Internal.Impl.contains (t.maxKeyD fallback) t = true
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Precomposing a co-Cartesian morphism with an isomorphism lifting the identity is
co-Cartesian.  -/
CategoryTheory.Functor.IsCocartesian.of_iso_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] {a' : 𝒳}
  (φ' : a' ≅ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ'.hom],
  p.IsCocartesian f (CategoryTheory.CategoryStruct.comp φ'.hom φ)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_union_le_aleph0 : ∀ {α : Type u_1} {P Q : Set α},
  Cardinal.mk ↑(P ∪ Q) ≤ Cardinal.aleph0 ↔ Cardinal.mk ↑P ≤ Cardinal.aleph0 ∧ Cardinal.mk ↑Q ≤ Cardinal.aleph0
-- Mathlib.Data.Finsupp.Basic
Finsupp.splitSupport.eq_1 : ∀ {ι : Type u_4} {M : Type u_5} {αs : ι → Type u_12} [inst : Zero M] (l : (i : ι) × αs i →₀ M),
  l.splitSupport = Finset.image Sigma.fst l.support
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_top : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜], ⊤.toIdeal = ⊤
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.match_1.congr_eq_1 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1) (x : ByteArray.utf8DecodeChar?.FirstByte)
  (h_1 : x = ByteArray.utf8DecodeChar?.FirstByte.invalid → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : x = ByteArray.utf8DecodeChar?.FirstByte.done → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : x = ByteArray.utf8DecodeChar?.FirstByte.oneMore → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : x = ByteArray.utf8DecodeChar?.FirstByte.twoMore → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : x = ByteArray.utf8DecodeChar?.FirstByte.threeMore → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore)
  (heq_1 : x = ByteArray.utf8DecodeChar?.FirstByte.invalid),
  (match h : x with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 h
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 h
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 h
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 h
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 h) ≍
    h_1 heq_1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.nat_tprod_vanishing : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G},
  Multipliable f → ∀ ⦃e : Set G⦄, e ∈ nhds 1 → ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (Std.DHashMap.ofList l).get? k' = some (cast ⋯ v)
-- Init.Data.BitVec.Lemmas
BitVec.getElem?_eq_getElem : ∀ {w : ℕ} {l : BitVec w} {n : ℕ} (h : n < w), l[n]? = some l[n]
-- Aesop.Util.UnorderedArraySet
/-- O(n)  -/
Aesop.UnorderedArraySet.filterM : {α : Type} →
  [inst : BEq α] →
    {m : Type → Type u_1} → [Monad m] → (α → m Bool) → Aesop.UnorderedArraySet α → m (Aesop.UnorderedArraySet α)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftLift.IsKan.uniqueUpToIso_inv_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.LeftLift f g} (P : s.IsKan) (Q : t.IsKan),
  CategoryTheory.StructuredArrow.Hom.right (P.uniqueUpToIso Q).inv = Q.desc s
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiRing_apply : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : Fintype ι] (z : M₂) (m : ι → R), (MultilinearMap.mkPiRing R ι z) m = (∏ i, m i) • z
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.adj_sub : ∀ {V : Type u} {G : SimpleGraph V} (self : G.Subgraph) {v w : V}, self.Adj v w → G.Adj v w
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `none` if the map is empty.
 -/
Std.DTreeMap.minKey? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → Option α
-- Init.Data.SInt.Lemmas
Int16.toInt.inj : ∀ {x y : Int16}, x.toInt = y.toInt → x = y
-- Mathlib.LinearAlgebra.Determinant
/-- Builds a linear equivalence from an endomorphism whose determinant is a unit.  -/
LinearMap.equivOfIsUnitDet : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [Module.Free R M] → [Module.Finite R M] → {f : M →ₗ[R] M} → IsUnit (LinearMap.det f) → M ≃ₗ[R] M
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instCoeTCOfSlashInvariantFormClass : {F : Type u_1} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {k : ℤ} → [inst : FunLike F UpperHalfPlane ℂ] → [SlashInvariantFormClass F Γ k] → CoeTC F (SlashInvariantForm Γ k)
-- Init.Data.Char.Lemmas
Char.toUInt8_val : ∀ {c : Char}, c.val.toUInt8 = c.toUInt8
-- Mathlib.Topology.Order.OrderClosed
/-- For any `a`, the set `(-∞, a]` is closed.  -/
ClosedIicTopology.isClosed_Iic : ∀ {α : Type u_1} {inst : TopologicalSpace α} {inst_1 : Preorder α} [self : ClosedIicTopology α] (a : α),
  IsClosed (Set.Iic a)
-- Mathlib.Topology.MetricSpace.IsometricSMul
nndist_add_right : ∀ {M : Type u} [inst : PseudoMetricSpace M] [inst_1 : Add M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M),
  nndist (a + c) (b + c) = nndist a b
-- Mathlib.Topology.Order.IsLUB
IsGLB.mem_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α} {s : Set α},
  IsGLB s a → s.Nonempty → IsClosed s → a ∈ s
-- Mathlib.Analysis.Normed.Module.Span
ContinuousLinearEquiv.coord_toSpanNonzeroSingleton : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {x : E} (h : x ≠ 0) (c : 𝕜),
  (ContinuousLinearEquiv.coord 𝕜 x h) ((ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h) c) = c