mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.absolutelyContinuous_ennreal_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α)
  (μ : MeasureTheory.VectorMeasure α ENNReal),
  MeasureTheory.VectorMeasure.AbsolutelyContinuous c μ ↔
    MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.re c) μ ∧
      MeasureTheory.VectorMeasure.AbsolutelyContinuous (MeasureTheory.ComplexMeasure.im c) μ
-- Std.Net.Addr
/-- The IP address assigned to the interface.
 -/
Std.Net.InterfaceAddress.address : Std.Net.InterfaceAddress → Std.Net.IPAddr
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algEquivOfAssociated_symm : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : Associated f g), (AdjoinRoot.algEquivOfAssociated R f g hfg).symm = AdjoinRoot.algEquivOfAssociated R g f ⋯
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.zero_of_eval_zero : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [Infinite R] (p : Polynomial R),
  (∀ (x : R), Polynomial.eval x p = 0) → p = 0
-- Lean.Util.Trace
Lean.MonadTrace.getTraceState : {m : Type → Type} → [self : Lean.MonadTrace m] → m Lean.TraceState
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Set`. See note [pointwise nat action].  -/
Set.NPow : {α : Type u_2} → [One α] → [Mul α] → Pow (Set α) ℕ
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRccSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRccSlice._auto_1) →
    Std.Rcc.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RccSlice α)
-- Mathlib.Order.SuccPred.CompleteLinearOrder
/-- Every conditionally complete linear order with well-founded `<` is a successor order, by setting
the successor of an element to be the infimum of all larger elements.  -/
ConditionallyCompleteLinearOrder.toSuccOrder : {α : Type u_2} → [inst : ConditionallyCompleteLinearOrder α] → [WellFoundedLT α] → SuccOrder α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = true → t.min! = default
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.one_le_divConst_self : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G}, A.Nonempty → 1 ≤ A.divConst A
-- Init.System.IO
/-- Creates a directory at the specified path. The parent directory must already exist.

Throws an exception if the directory cannot be created.
 -/
IO.FS.createDir : System.FilePath → IO Unit
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.ofSet_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} (hs : IsOpen s),
  (OpenPartialHomeomorph.ofSet s hs).symm = OpenPartialHomeomorph.ofSet s hs
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_same : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α), gcd a a = normalize a
-- Init.Data.String.Lemmas.Pattern.Split.Char
String.toList_split_intercalate_beq : ∀ {c : Char} {l : List String},
  (∀ s ∈ l, c ∉ s.toList) →
    ((((String.singleton c).intercalate l).split c).toList ==
        if l = [] then ["".toSlice] else List.map String.toSlice l) =
      true
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey!_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.ExtDHashMap.filterMap f m).getKey! k =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (Std.ExtDHashMap.Const.get m x_2 ⋯)).isSome).get!
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
BoundedContinuousFunction.coeFn_toLp : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} (p : ENNReal) (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ] (𝕜 : Type u_3)
  [inst_5 : Fact (1 ≤ p)] [inst_6 : NormedRing 𝕜] [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E]
  (f : BoundedContinuousFunction α E), ↑↑((BoundedContinuousFunction.toLp p μ 𝕜) f) =ᵐ[μ] ⇑f
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.eq_1 : ∀ {α : Type u} [uniformSpace : UniformSpace α] (f : Filter α), Cauchy f = (f.NeBot ∧ f ×ˢ f ≤ uniformity α)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_insert_of_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v' v : α} [Std.TransCmp cmp] (t : RBTree.RBSet α cmp),
  cmp v' v = Ordering.eq → (t.insert v).find? v' = some v
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coeAddHom_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (a : NormedAddGroupHom V₁ V₂) (a_1 : V₁), NormedAddGroupHom.coeAddHom a a_1 = a a_1
-- Mathlib.RingTheory.MatrixAlgebra
Matrix.kroneckerTMulStarAlgEquiv_symm_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_5) (S : Type u_6) {A : Type u_7} {B : Type u_8} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Fintype n]
  [inst_6 : DecidableEq n] [inst_7 : CommSemiring S] [inst_8 : Algebra R S] [inst_9 : Algebra S A]
  [inst_10 : IsScalarTower R S A] [inst_11 : Fintype m] [inst_12 : DecidableEq m] [inst_13 : StarRing R]
  [inst_14 : StarAddMonoid A] [inst_15 : StarAddMonoid B] [inst_16 : StarModule R A] [inst_17 : StarModule R B]
  (x : Matrix (m × n) (m × n) (TensorProduct R A B)),
  (Matrix.kroneckerTMulStarAlgEquiv m n R S A B).symm x = (kroneckerTMulLinearEquiv m m n n R S A B).symm x
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.AllZero.eq_1 : ∀ (m : Tactic.ComputeAsymptotics.UnitMonomial), m.AllZero = (m.sign = Tactic.ComputeAsymptotics.UnitMonomial.Sign.zero)
-- Mathlib.ModelTheory.PartialEquiv
/-- Given a partial equivalence which has the whole structure as domain,
returns the corresponding embedding.  -/
FirstOrder.Language.PartialEquiv.toEmbeddingOfEqTop : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → {f : L.PartialEquiv M N} → f.dom = ⊤ → L.Embedding M N
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.epi_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → S.g = 0 → CategoryTheory.Epi S.f
-- Mathlib.Order.Bounds.Basic
bddAbove_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddAbove (Set.Ioc b a)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] (f : α → β) (c : α), Function.Periodic f c = ∀ (x : α), f (x + c) = f x
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Restriction of an `AddMonoidHom` to an `AddSubmonoid` of the codomain.  -/
AddMonoidHom.codRestrict : {M : Type u_1} →
  {N : Type u_2} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        {S : Type u_5} →
          [inst_2 : SetLike S N] →
            [inst_3 : AddSubmonoidClass S N] → (f : M →+ N) → (s : S) → (∀ (x : M), f x ∈ s) → M →+ ↥s
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData'_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p),
  (CochainComplex.HomComplex.leftHomologyData' K L n m p hm hp).π =
    AddCommGrpCat.ofHom (CochainComplex.HomComplex.CohomologyClass.mkAddMonoidHom K L m)
-- Mathlib.MeasureTheory.Integral.Marginal
Measurable.lmarginal : ∀ {δ : Type u_1} {X : δ → Type u_3} [inst : (i : δ) → MeasurableSpace (X i)] (μ : (i : δ) → MeasureTheory.Measure (X i))
  [inst_1 : DecidableEq δ] {s : Finset δ} {f : ((i : δ) → X i) → ENNReal} [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)],
  Measurable f → Measurable (∫⋯∫⁻_s, f ∂μ)
-- Mathlib.CategoryTheory.Products.Basic
/-- The unit isomorphism for `functorProdFunctorEquiv`  -/
CategoryTheory.functorProdFunctorEquivUnitIso : (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] →
            CategoryTheory.Functor.id (CategoryTheory.Functor A B × CategoryTheory.Functor A C) ≅
              (CategoryTheory.prodFunctorToFunctorProd A B C).comp (CategoryTheory.functorProdToProdFunctor A B C)
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphere_apply_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) (s : Set ↑(Metric.sphere 0 1)) (r : ↑(Set.Ioi 0)),
  μ (Subtype.val '' ⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Set.Iio r) = μ (Set.Ioo 0 ↑r • Subtype.val '' s)
-- Mathlib.Order.InitialSeg
/-- For any two well orders, one is an initial segment of the other.  -/
InitialSeg.total : {α : Type u_1} →
  {β : Type u_2} →
    (r : α → α → Prop) → (s : β → β → Prop) → [IsWellOrder α r] → [IsWellOrder β s] → InitialSeg r s ⊕ InitialSeg s r
-- Mathlib.RingTheory.Jacobson.Ring
Polynomial.instIsJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R], IsJacobsonRing (Polynomial R)
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.neg_right : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → IsRelPrime x (-y)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_roo_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n - (m + 1)).toNat ≤ i → (m<...n).toList.getD i fallback = fallback
-- Mathlib.Algebra.GroupWithZero.Nat
Nat.instMonoidWithZero : MonoidWithZero ℕ
-- Init.Data.Array.Lemmas
Array.any_flatten' : ∀ {α : Type u_1} {stop : ℕ} {f : α → Bool} {xss : Array (Array α)},
  stop = xss.flatten.size → xss.flatten.any f 0 stop = xss.any fun x => x.any f
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- The `MonoOver Y` for the image inclusion for a morphism `f : X ⟶ Y`.
 -/
CategoryTheory.MonoOver.imageMonoOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasImage f] → CategoryTheory.MonoOver Y
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.zpowersEquivSupport.congr_simp : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α} (hσ : σ.IsCycle),
  hσ.zpowersEquivSupport = hσ.zpowersEquivSupport
-- Mathlib.LinearAlgebra.AffineSpace.Basis
fintypeAffineCoords.eq_1 : ∀ (ι : Type u_1) (k : Type u_2) [inst : Ring k] [inst_1 : Fintype ι],
  fintypeAffineCoords ι k = AffineSubspace.comap (Fintype.linearCombination k 1).toAffineMap (affineSpan k {1})
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertManyIfNewUnit l).getKey? k' = some k
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuous_invFun : ∀ {𝕜 : 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.invFun
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborates the negative of an `OfNat.ofNat` literal.
`-@OfNat.ofNat _ n _` ~> `-n`
 -/
Lean.PrettyPrinter.Delaborator.delabNeg : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.autCongr_trans : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₂ ≃ₐ[R] A₃), ϕ.autCongr.trans ψ.autCongr = (ϕ.trans ψ).autCongr
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] (n : ℕ),
  CategoryTheory.CategoryStruct.comp
      (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
      (CategoryTheory.CategoryStruct.comp
        ((s.cofan (Opposite.op { len := n })).inj
          (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
        (AlgebraicTopology.DoldKan.PInfty.f n)) =
    AlgebraicTopology.DoldKan.PInfty.f n
-- Mathlib.Topology.UniformSpace.Separation
Filter.Tendsto.inseparable_iff_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {β : Type u_1} {l : Filter β} [l.NeBot] {f g : β → α} {a b : α},
  Filter.Tendsto f l (nhds a) →
    Filter.Tendsto g l (nhds b) → (Inseparable a b ↔ Filter.Tendsto (fun x => (f x, g x)) l (uniformity α))
-- Mathlib.Data.Set.Image
/-- image and preimage are a Galois connection  -/
Set.image_subset_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, f '' s ⊆ t ↔ s ⊆ f ⁻¹' t
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (x : ↥X) (hxU : x ∈ U) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) (CategoryTheory.CategoryStruct.comp U.toSpecΓ h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.germ U x hxU)) h
-- Init.Data.SInt.Basic
/-- Signed integers that are the size of a word on the platform's architecture.

On a 32-bit architecture, `ISize` is equivalent to `Int32`. On a 64-bit machine, it is equivalent to
`Int64`. This type has special support in the compiler so it can be represented by an unboxed value.
 -/
ISize : Type
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- The measure of a disjoint union (even uncountable) of measurable sets is at least the sum of
the measures of the sets.  -/
MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint : ∀ {α : Type u_1} {ι : Type u_8} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α},
  (∀ (i : ι), MeasurableSet (As i)) → Pairwise (Function.onFun Disjoint As) → ∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)
-- Mathlib.Topology.Homotopy.Affine
ContinuousMap.Homotopy.affine_apply : ∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : IsTopologicalAddGroup E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] (f g : C(X, E))
  (x : ↑unitInterval × X), (ContinuousMap.Homotopy.affine f g) x = (AffineMap.lineMap (f x.2) (g x.2)) ↑x.1
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'.eq_def : ∀ {α : Type u_1} (x : RegularExpression α),
  x.matches' =
    match x with
    | RegularExpression.zero => 0
    | RegularExpression.epsilon => 1
    | RegularExpression.char a => {[a]}
    | P.plus Q => P.matches' + Q.matches'
    | P.comp Q => P.matches' * Q.matches'
    | P.star => KStar.kstar P.matches'
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- Auxiliary function to defining negation multiplication on tensor product.  -/
TensorProduct.Neg.aux : (R : Type u_1) →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      {N : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → TensorProduct R M N →ₗ[R] TensorProduct R M N
-- Mathlib.CategoryTheory.EqToHom
/-- An equality `X = Y` gives us an isomorphism `X ≅ Y`.

It is typically better to use this, rather than rewriting by the equality then using `Iso.refl _`
which usually leads to dependent type theory hell.
 -/
CategoryTheory.eqToIso : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → X = Y → (X ≅ Y)
-- Mathlib.Order.Filter.Cocardinal
Finset.eventually_cocardinal_notMem : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (s : Finset α), ∀ᶠ (x : α) in Filter.cocardinal α hreg, x ∉ s
-- Lean.Elab.DefView
Lean.Elab.instInhabitedDefView : Inhabited Lean.Elab.DefView
-- Mathlib.Data.ZMod.Basic
ZMod.charZero : CharZero (ZMod 0)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toArray_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → Option γ},
  t.WF →
    (Std.TreeMap.Raw.filterMap f t).toArray =
      Array.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) t.toArray
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- **Alias** of `tendsto_inv_iff`. -/
ENNReal.tendsto_inv_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {l : Filter α}
  {m : α → G} {a : G}, Filter.Tendsto (fun x => (m x)⁻¹) l (nhds a⁻¹) ↔ Filter.Tendsto m l (nhds a)
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_cons_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → (a ::ₘ s).dedup = s.dedup
-- Init.Data.String.Search
/-- Finds the position of the first match of the pattern `pattern` in after the position
`pos`. If there is no match `none` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".startPos.find? Char.isWhitespace).map (·.get!) == some ' '`

* `("tea".pos ⟨1⟩ (by decide)).find? (fun (c : Char) => c == 't') == none`
 -/
String.Pos.find? : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        {s : String} → s.Pos → (pattern : ρ) → [String.Slice.Pattern.ToForwardSearcher pattern σ] → Option s.Pos
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.mk.inj : ∀ {α : Type u_1} {inst : MetricSpace α} {N : ℕ} {τ : ℝ} {c : Fin N.succ → α} {r : Fin N.succ → ℝ}
  {rpos : ∀ (i : Fin N.succ), 0 < r i}
  {h : Pairwise fun i j => r i ≤ dist (c i) (c j) ∧ r j ≤ τ * r i ∨ r j ≤ dist (c j) (c i) ∧ r i ≤ τ * r j}
  {hlast : ∀ i < Fin.last N, r i ≤ dist (c i) (c (Fin.last N)) ∧ r (Fin.last N) ≤ τ * r i}
  {inter : ∀ i < Fin.last N, dist (c i) (c (Fin.last N)) ≤ r i + r (Fin.last N)} {c_1 : Fin N.succ → α}
  {r_1 : Fin N.succ → ℝ} {rpos_1 : ∀ (i : Fin N.succ), 0 < r_1 i}
  {h_1 :
    Pairwise fun i j =>
      r_1 i ≤ dist (c_1 i) (c_1 j) ∧ r_1 j ≤ τ * r_1 i ∨ r_1 j ≤ dist (c_1 j) (c_1 i) ∧ r_1 i ≤ τ * r_1 j}
  {hlast_1 : ∀ i < Fin.last N, r_1 i ≤ dist (c_1 i) (c_1 (Fin.last N)) ∧ r_1 (Fin.last N) ≤ τ * r_1 i}
  {inter_1 : ∀ i < Fin.last N, dist (c_1 i) (c_1 (Fin.last N)) ≤ r_1 i + r_1 (Fin.last N)},
  { c := c, r := r, rpos := rpos, h := h, hlast := hlast, inter := inter } =
      { c := c_1, r := r_1, rpos := rpos_1, h := h_1, hlast := hlast_1, inter := inter_1 } →
    c = c_1 ∧ r = r_1
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.withDensity_rnDeriv_of_subset_mutuallySingularSetSlice : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel κ]
  [inst : ProbabilityTheory.IsFiniteKernel η] {a : α} {s : Set γ},
  s ⊆ κ.mutuallySingularSetSlice η a → ((η.withDensity (κ.rnDeriv η)) a) s = 0
-- Mathlib.Combinatorics.Hindman
Hindman.FS.brecOn : ∀ {M : Type u_1} [inst : AddSemigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FS a a_1 → Prop}
  {a : Stream' M} {a_1 : M} (t : Hindman.FS a a_1),
  (∀ (a : Stream' M) (a_2 : M) (t : Hindman.FS a a_2), Hindman.FS.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.Algebra.Homology.ShortComplex.Limits
/-- If a cone with values in `ShortComplex C` is such that it becomes limit
when we apply the three projections `ShortComplex C ⥤ C`, then it is limit.  -/
CategoryTheory.ShortComplex.isLimitOfIsLimitπ : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          {F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} →
            (c : CategoryTheory.Limits.Cone F) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₁.mapCone c) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₂.mapCone c) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.ShortComplex.π₃.mapCone c) →
                    CategoryTheory.Limits.IsLimit c
-- Mathlib.Data.Fintype.Sigma
Set.biInter_finsetSigma_univ' : ∀ {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_3} [inst : (i : ι) → Fintype (κ i)] (s : Finset ι)
  (f : (i : ι) → κ i → Set α), ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun x => Finset.univ, f ij.fst ij.snd
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.map_swap_antidiagonal : ∀ {α : Type u_1} (s : Multiset α), Multiset.map Prod.swap s.antidiagonal = s.antidiagonal
-- Mathlib.LinearAlgebra.LinearPMap
/-- For a family of (semi)linear maps with a directed domains such that the one defined on a larger
domain restricts to the one defined on the smaller domain, this defines the (semi)linear map defined
on the union of the domains extending all the (semi)linear maps in the family.  -/
LinearPMap.sSup : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module S F] → (c : Set (E →ₛₗ.[σ] F)) → DirectedOn (fun x1 x2 => x1 ≤ x2) c → E →ₛₗ.[σ] F
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.instIsGeneratedByOneHypercovers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  J.IsGeneratedByOneHypercovers
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearYoneda_map_app : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : Cᵒᵖ),
  ((CategoryTheory.linearYoneda R C).map f).app Y =
    ModuleCat.ofHom (CategoryTheory.Linear.rightComp R (Opposite.unop Y) f)
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory CommSemiRingCat fun R S => ↑R →+* ↑S
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the second kind (Vieta–Fibonacci polynomial)
evaluates on `2 * cosh θ` to the value `sinh ((n + 1) * θ) / sinh θ`.  -/
Polynomial.Chebyshev.S_two_mul_complex_cosh : ∀ (θ : ℂ) (n : ℤ),
  Polynomial.eval (2 * Complex.cosh θ) (Polynomial.Chebyshev.S ℂ n) * Complex.sinh θ = Complex.sinh ((↑n + 1) * θ)
-- Mathlib.Algebra.Group.PNatPowAssoc
Pi.instPNatPowAssoc : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Mul (α i)] [inst_1 : (i : ι) → Pow (α i) ℕ+]
  [∀ (i : ι), PNatPowAssoc (α i)], PNatPowAssoc ((i : ι) → α i)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.embedding_of_isReal_apply : ∀ {K : Type u_1} [inst : Field K] {w : NumberField.InfinitePlace K} (hw : w.IsReal) (x : K),
  ↑((NumberField.InfinitePlace.embedding_of_isReal hw) x) = w.embedding x
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m.keysArray.contains k = m.contains k
-- Lean.Elab.Do.Basic
Lean.Elab.Do.elabNestedAction : Lean.Elab.Term.TermElab