mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instUniformSpace : {X : Type u_1} →
  {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [UniformSpace X] → UniformSpace (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.Quotient.coe_smul_out : ∀ {G : Type u} {X : Type v} [inst : Group G] [inst_1 : Monoid X] [inst_2 : MulAction X G] (H : Subgroup G)
  [inst_3 : MulAction.QuotientAction X H] (b : X) (q : G ⧸ H), ↑(b • Quotient.out q) = b • q
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map_comp_inl : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn),
  (SemidirectProduct.map fn fg h).comp SemidirectProduct.inl = SemidirectProduct.inl.comp fn
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (carrier : TopCat) (presheaf : TopCat.Presheaf C carrier)
  (carrier_1 : TopCat) (presheaf_1 : TopCat.Presheaf C carrier_1),
  ({ carrier := carrier, presheaf := presheaf } = { carrier := carrier_1, presheaf := presheaf_1 }) =
    (carrier = carrier_1 ∧ presheaf ≍ presheaf_1)
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- `f` is an effective epi  -/
CategoryTheory.Functor.EffectivePresentation.effectiveEpi : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {X : D}
  (self : F.EffectivePresentation X), CategoryTheory.EffectiveEpi self.f
-- Mathlib.Algebra.Algebra.Hom
/-- Defining the homomorphism in the category R-Alg, denoted `A →ₐ[R] B`.  -/
AlgHom : (R : Type u) →
  (A : Type v) →
    (B : Type w) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Semiring B] → [Algebra R A] → [Algebra R B] → Type (max v w)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₀ F₁ F₂ : CategoryTheory.Functor C C} (α : F₀ ⟶ F₁)
  (β : F₁ ⟶ F₂) (X : CategoryTheory.Endofunctor.Algebra F₂),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp α β).hom.app X).f = CategoryTheory.CategoryStruct.id X.a
-- Mathlib.Topology.UniformSpace.OfFun
/-- Define a `UniformSpace` using a "distance" function. The function can be, e.g., the
distance in a (usual or extended) metric space or an absolute value on a ring. We assume that
there is a preexisting topology, for which the neighborhoods can be expressed using the "distance",
and we make sure that the uniform space structure we construct has a topology which is defeq
to the original one.  -/
UniformSpace.ofFunOfHasBasis : {X : Type u_1} →
  {M : Type u_2} →
    [t : TopologicalSpace X] →
      [inst : AddCommMonoid M] →
        [inst_1 : LinearOrder M] →
          (d : X → X → M) →
            (∀ (x : X), d x x = 0) →
              (∀ (x y : X), d x y = d y x) →
                (∀ (x y z : X), d x z ≤ d x y + d y z) →
                  (∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε) →
                    (∀ (x : X), (nhds x).HasBasis (fun ε => 0 < ε) fun ε => {y | d x y < ε}) → UniformSpace X
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.le_size_of_le_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α β f] {x : ℕ}
  (aig : Std.Sat.AIG α) (input : β aig), x ≤ aig.decls.size → x ≤ (f aig input).aig.decls.size
-- Mathlib.Logic.Basic
xor_self : ∀ (a : Prop), Xor a a = False
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuous_toFun : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (self : ModelWithCorners 𝕜 E H),
  Continuous ↑self.toPartialEquiv
-- Mathlib.Algebra.BigOperators.Expect
/-- Reorder an average.

The difference with `Finset.expect_bij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.expect_nbij` is that the bijection is allowed to use membership of the
domain of the average, rather than being a non-dependent function.  -/
Finset.expect_bij : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] {s : Finset ι}
  {f : ι → M} {t : Finset κ} {g : κ → M} (i : (a : ι) → a ∈ s → κ),
  (∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) →
    (∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) →
      (∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
        (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) → (s.expect fun i => f i) = t.expect fun i => g i
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.comap_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M M' : CategoryTheory.Functor C MonCat} (p : M ⟶ M')
  (S' : CategoryTheory.SubmonoidFunctor M') (x : C),
  (CategoryTheory.SubmonoidFunctor.comap p S').obj x = Submonoid.comap (MonCat.Hom.hom (p.app x)) (S'.obj x)
-- Init.Prelude
instInhabitedNat : Inhabited ℕ
-- Mathlib.NumberTheory.FLT.Four
Fermat42.ne_zero : ∀ {a b c : ℤ}, Fermat42 a b c → c ≠ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
/-- Abbreviation for multicoequalizer diagrams in the complete lattice of
subcomplexes of a simplicial set.  -/
SSet.Subcomplex.MulticoequalizerDiagram : {X : SSet} → X.Subcomplex → {ι : Type u_1} → (ι → X.Subcomplex) → (ι → ι → X.Subcomplex) → Prop
-- Mathlib.CategoryTheory.Functor.Category
/-- Notation for horizontal composition of natural transformations.  -/
CategoryTheory.NatTrans.«term_◫_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_top : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  [inst_3 : FaithfulSMul M X], ↑⊤ = 1
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given a simple function `f` with values in `ℝ≥0`, there exists a lower semicontinuous
function `g ≥ f` with integral arbitrarily close to that of `f`. Formulation in terms of
`lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] (μ : MeasureTheory.Measure α)
  [μ.WeaklyRegular] (f : MeasureTheory.SimpleFunc α NNReal) {ε : ENNReal},
  ε ≠ 0 → ∃ g, (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanModuleHierarchyImportedByParams.mk : Lean.Lsp.LeanModule → Lean.Lsp.LeanModuleHierarchyImportedByParams
-- Batteries.Data.String.Legacy
/-- Applies the function `f` to every character in a string, returning a string that contains the
resulting characters.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`. Its runtime behavior is equivalent to that of `String.map`.

Examples:
 * `"abc123".map Char.toUpper = "ABC123"`
 * `"".map Char.toUpper = ""`
 -/
String.Legacy.map : (Char → Char) → String → String
-- Mathlib.Analysis.SpecialFunctions.FrullaniIntegral
Frullani.intervalIntegrable_inv_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ},
  MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
    0 < a → 0 < b → IntervalIntegrable (fun x => x⁻¹ • f x) MeasureTheory.volume a b
-- Mathlib.RingTheory.MvPowerSeries.LexOrder
MvPowerSeries.lexOrder.congr_simp : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : LinearOrder σ] [inst_2 : WellFoundedGT σ]
  (φ φ_1 : MvPowerSeries σ R), φ = φ_1 → φ.lexOrder = φ_1.lexOrder
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.pow_eq : ∀ {R : Type u_1} {p : R} [inst : Monoid R] [inst_1 : Star R], IsStarProjection p → ∀ {n : ℕ}, n ≠ 0 → p ^ n = p
-- Mathlib.Order.Hom.WithTopBot
SupHom.withBot'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] [inst_2 : OrderBot β]
  (f : SupHom α β) (a : WithBot α), f.withBot' a = Option.elim a ⊥ ⇑f
-- Mathlib.RingTheory.Congruence.Hom
RingCon.congr_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M}
  {d : RingCon N} (e : M ≃+* N) (h : c = d.comap e) (a : M), (RingCon.congr e h) ↑a = ↑(e a)
-- Init.Data.List.Lemmas
List.foldr_filterMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ → γ} {l : List α} {init : γ},
  List.foldr g init (List.filterMap f l) =
    List.foldr
      (fun x y =>
        match f x with
        | some b => g b y
        | none => y)
      init l
-- Mathlib.Logic.Equiv.List
/-- If `α` is countable, then so is `Finset α`.  -/
Finset.countable : ∀ {α : Type u_1} [Countable α], Countable (Finset α)
-- Mathlib.Algebra.Order.Archimedean.Basic
Archimedean.comap : ∀ {G : Type u_1} {M : Type u_2} [inst : AddCommMonoid G] [inst_1 : LinearOrder G] [inst_2 : AddCommMonoid M]
  [inst_3 : PartialOrder M] [Archimedean M] (f : G →+ M), StrictMono ⇑f → Archimedean G
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.instSetLike : (A : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing A] → [inst_1 : LieRing L] → [inst_2 : Module A L] → SetLike (LieRinehartSubalgebra A L) L
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHom_whisker_exchange_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X X' Y Y' : C}
  (f : X ⟶ X') (g : Y ⟶ Y') {Z : V} (h : (X ⟶[V] Y') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X' g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f Y') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X g) h)
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The forgetful functor from R-modules to types preserves all limits.
 -/
ModuleCat.forget_preservesLimitsOfSize : ∀ {R : Type u} [inst : Ring R] [UnivLE.{v, w}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, v, w, w, max u (w + 1), w + 1} (CategoryTheory.forget (ModuleCat R))
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
/-- There is a zero map from any module with the zero form.  -/
LinearMap.BilinForm.Isometry.instZeroOfNat : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] → [inst_4 : Module R M₂] → {B₂ : LinearMap.BilinForm R M₂} → Zero (0 →bᵢ B₂)
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_sorted : ∀ (n : ℕ), n.primeFactorsList.SortedLE
-- Mathlib.Condensed.Discrete.Basic
LightCondensed.underlying_map : ∀ (C : Type w) [inst : CategoryTheory.Category.{u, w} C]
  {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) C} (f : X ⟶ Y),
  (LightCondensed.underlying C).map f = f.hom.app (Opposite.op (LightProfinite.of PUnit.{u + 1}))
-- Mathlib.FieldTheory.Extension
IntermediateField.nonempty_algHom_adjoin_of_splits : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E},
  (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    Nonempty (↥(IntermediateField.adjoin F S) →ₐ[F] K)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.analyticAt_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ), AnalyticAt ℂ (L.derivWeierstrassPExcept l₀) l₀
-- Init.Tactics
/-- `exists e₁, e₂, ...` is shorthand for `refine ⟨e₁, e₂, ...⟩; try trivial`.
It is useful for existential goals.
 -/
Lean.Parser.Tactic.«tacticExists_,,» : Lean.ParserDescr
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.instLawfulMonad : LawfulMonad PMF
-- Lean.Data.Json.FromToJson.Extra
Lean.instFromJsonTreeMapString : {α : Type} → {cmp : String → String → Ordering} → [Lean.FromJson α] → Lean.FromJson (Std.TreeMap String α cmp)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.excenter_notMem_affineSpan_pair : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} [n.AtLeastTwo]
  {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs → ∀ (i j : Fin (n + 1)), s.excenter signs ∉ line[ℝ, s.points i, s.points j]
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert!.size.eq_2 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.containsThenInsert!.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') = size
-- Lean.Parser.Term
Lean.Parser.Term.doubleQuotedName.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.Measure.ext_of_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α),
  (∀ (f : α → ENNReal), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν) → μ = ν
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.hasLimit : ∀ {C : Type u₁} {D : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W] (X : C) [F.HasPointwiseLeftDerivedFunctorAt W X], L.HasPointwiseRightKanExtensionAt F (L.obj X)
-- Mathlib.CategoryTheory.Category.Basic
/-- A thin wrapper for `aesop` which adds the `CategoryTheory` rule set and
allows `aesop` to look through semireducible definitions when calling `intros`.
This tactic fails when it is unable to solve the goal, making it suitable for
use in auto-params.
 -/
CategoryTheory.aesop_cat : Lean.ParserDescr
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.MVarValue.mvarId.inj : ∀ {mvarId mvarId_1 : Lean.MVarId},
  Aesop.EqualUpToIds.MVarValue.mvarId mvarId = Aesop.EqualUpToIds.MVarValue.mvarId mvarId_1 → mvarId = mvarId_1
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Cfg.mk : {Γ : Type u_1} →
  {Λ : Type u_2} → {σ : Type u_3} → [inst : Inhabited Γ] → Option Λ → σ → Turing.Tape Γ → Turing.TM1.Cfg Γ Λ σ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_cons : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {l : List ((a : α) × β a)} {k : α} {v : β k}, ↑(m.insertMany (⟨k, v⟩ :: l)) = ↑((m.insert k v).insertMany l)
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.neg_fst : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A),
  (-a).toProd.1 = -a.toProd.1
-- Mathlib.Computability.TuringDegree
instIsPreorderPFunNatTuringReducible : IsPreorder (ℕ →. ℕ) TuringReducible
-- Batteries.Data.List.Basic
/-- `dropSuffix? l s` returns
`some r` if `l = r ++ s'` for some `s'` which is paiwise `==` to `s`,
and `none` otherwise.  -/
List.dropSuffix? : {α : Type u_1} → [BEq α] → List α → List α → Option (List α)
-- Mathlib.Data.SetLike.Basic
SetLike.instMembership : {A : Type u_1} → {B : Type u_2} → [i : SetLike A B] → Membership B A
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsMultiplicativeWeakEquivalencesOfIsWeakFactorizationSystemTrivialCofibrationsFibrationsOfIsStableUnderRetractsOfIsStableUnderComposition : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderRetracts]
  [(HomotopicalAlgebra.weakEquivalences C).IsStableUnderComposition],
  (HomotopicalAlgebra.weakEquivalences C).IsMultiplicative
-- Mathlib.Data.FinEnum
FinEnum.PSigma.finEnumPropRight : {α : Type u} → {β : α → Prop} → [FinEnum α] → [(a : α) → Decidable (β a)] → FinEnum ((a : α) ×' β a)
-- Mathlib.Data.Set.Finite.Lattice
Set.fintypeiUnion : {α : Type u} →
  {ι : Sort w} →
    [DecidableEq α] → [Fintype (PLift ι)] → (f : ι → Set α) → [(i : ι) → Fintype ↑(f i)] → Fintype ↑(⋃ i, f i)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skipWhile_eq_iff : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} (startPos endPos : s.Pos),
  startPos.skipWhile pat = endPos ↔
    String.Slice.Pattern.Model.IsLongestMatchAtChain pat startPos endPos ∧
      (¬String.Slice.Pattern.Model.MatchesAt pat endPos ∨ String.Slice.Pattern.Model.IsLongestMatchAt pat endPos endPos)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply_superset : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, s ⊆ t → (μ.restrict s) t = μ s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
  [inst_2 : Inhabited (β k)] {v : β k}, Std.Internal.List.getValueCast! k (Std.Internal.List.insertEntry k v l) = v
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.sum_finsupport : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) {x₀ : X},
  x₀ ∈ s → ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1
-- Init.Data.BitVec.Lemmas
BitVec.allOnes_and : ∀ {w : ℕ} {x : BitVec w}, BitVec.allOnes w &&& x = x
-- Lean.Elab.DefView
Lean.Elab.DefView : Type
-- Mathlib.Data.Prod.TProd
/-- Given an element of the iterated product `l.Prod α`, take a projection into direction `i`.
If `i` appears multiple times in `l`, this chooses the first component in direction `i`.  -/
List.TProd.elim : {ι : Type u} → {α : ι → Type v} → [DecidableEq ι] → {l : List ι} → List.TProd α l → {i : ι} → i ∈ l → α i
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.coprod.desc_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F₁ F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ ⟶ F)
  (τ₂ : F₂ ⟶ F),
  CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inr
      (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂) =
    τ₂
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.separator.congr_simp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.HasSeparator C],
  CategoryTheory.separator C = CategoryTheory.separator C
-- Init.Data.BitVec.Lemmas
BitVec.msb_shiftLeft : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, (x <<< n).msb = x.getMsbD n
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMap.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (out' : γ) (h_1 : some out' = none → motive none)
  (h_2 : (out'_1 : γ) → some out' = some out'_1 → motive (some out'_1)),
  (match h' : some out' with
    | none => h_1 h'
    | some out'_1 => h_2 out'_1 h') =
    h_2 out' ⋯
-- Mathlib.AlgebraicGeometry.Birational.Dominant
AlgebraicGeometry.Scheme.RationalMap.IsDominant.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X.RationalMap Y},
  Quotient.liftOn f (fun g => AlgebraicGeometry.IsDominant g.hom) ⋯ → f.IsDominant
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.toAbs_inv : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] (v : AbsoluteValue R S)
  (x : R), WithAbs.toAbs v x⁻¹ = (WithAbs.toAbs v x)⁻¹
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.erasePTR.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.erasePTR p l = List.erasePTR.go✝ p l l #[]
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsInducing.mem_functorObj_iff : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑X) {x : ↑X}, (CategoryTheory.ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ U
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- `pointIndex` as an embedding.  -/
Affine.Simplex.pointIndexEmbedding : (n : ℕ) → Fin (n + 1) ↪ Affine.Simplex.PointsWithCircumcenterIndex n
-- Init.Data.SInt.Bitwise
Int64.toUInt64_not : ∀ (a : Int64), (~~~a).toUInt64 = ~~~a.toUInt64
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.mk_mem_unramifiedPlacesOver : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {φ : L →+* ℂ},
  φ ∈ NumberField.ComplexEmbedding.unmixedEmbeddingsOver L v.embedding →
    NumberField.InfinitePlace.mk φ ∈ NumberField.InfinitePlace.unramifiedPlacesOver L v
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) (h : n + 1 = m),
  CochainComplex.mappingCone.liftCochain φ α β h =
    α.comp (CochainComplex.mappingCone.inl φ) ⋯ +
      β.comp (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k k' : α} {f : Option (β k) → Option (β k)},
  m.WF → (m.alter k f).contains k' = if (k == k') = true then (f (m.get? k)).isSome else m.contains k'
-- Mathlib.Topology.Category.LightProfinite.Basic
lightDiagramToLightProfinite_obj : ∀ (X : LightDiagram), lightDiagramToLightProfinite.obj X = LightProfinite.of ↑X.cone.pt.toTop
-- Mathlib.Topology.Defs.Sequences
/-- A function between topological spaces is sequentially continuous if it commutes with limit of
convergent sequences.  -/
SeqContinuous : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Lean.Meta.Tactic.Util
Lean.Meta.tactic.skipAssignedInstances : Lean.Option Bool
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instNonUnitalSubringClass : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : NonUnitalNonAssocRing A] [inst_2 : Module R A],
  NonUnitalSubringClass (NonUnitalSubalgebra R A) A
-- Mathlib.RingTheory.Valuation.Basic
Valuation.restrict_eq_one_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R}, v.restrict x = 1 ↔ v x = 1
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Turn a morphism in `Rep` back into an `IntertwiningMap`.  -/
Rep.Hom.hom : {k : Type u} →
  {G : Type v} →
    [inst : Semiring k] → [inst_1 : Monoid G] → {A B : Rep.{w, u, v} k G} → A.Hom B → A.ρ.IntertwiningMap B.ρ