mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.keys_filter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Bool} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).keys.Perm
    (List.filter
        (fun x =>
          match x with
          | ⟨x, h'⟩ => f x (Std.DHashMap.Raw.Const.get m x ⋯))
        m.keys.attach).unattach
-- Mathlib.Computability.TuringMachine.Tape
/-- The current position of the head.  -/
Turing.Tape.head : {Γ : Type u_1} → [inst : Inhabited Γ] → Turing.Tape Γ → Γ
-- Mathlib.Algebra.Ring.Ext
NonUnitalCommRing.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalCommRing R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.Hom.ext_iff : ∀ {R : Type u} {inst : CommRing R} {V W : BialgCat R} {x y : V.Hom W}, x = y ↔ x.toBialgHom' = y.toBialgHom'
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation_G : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (exteriorPower.presentation R n M).G = (Fin n → M)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.coe_smul : ∀ (g : GL (Fin 2) ℝ) (z : UpperHalfPlane),
  ↑(g • z) = (UpperHalfPlane.σ g) (UpperHalfPlane.num g ↑z / UpperHalfPlane.denom g ↑z)
-- Mathlib.Data.Set.Disjoint
/-- **Alias** of the forward direction of `Set.disjoint_iff_forall_ne`. -/
Disjoint.ne_of_mem : ∀ {α : Type u} {s t : Set α}, Disjoint s t → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ t → a ≠ b
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.isoMk_hom_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map r.hom))
      CategoryTheory.MorphismProperty.Comma.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Comma.isoMk l r h).hom.left = l.hom
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.iInter_halfSpaces_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E}
  [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E], Convex ℝ s → IsClosed s → ⋂ l, {x | ∃ y ∈ s, RCLike.re (l x) ≤ RCLike.re (l y)} = s
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_X_pow : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] (n : ℕ) [inst_2 : MulSemiringAction (Multiplicative ℕ) R],
  (SkewPolynomial.X ^ n).support = {n}
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsSMulApplyNat : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsSMulApply ℕ (SchwartzMap E F) E F
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProdAssoc_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (G : SimpleGraph α) (H : SimpleGraph β) (I : SimpleGraph γ)
  (p : (α × β) × γ), (G.boxProdAssoc H I) p = (p.1.1, p.1.2, p.2)
-- Mathlib.Algebra.Star.Unitary
Unitary.val_inv_toUnits_apply : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] (x : ↥(unitary R)), ↑(Unitary.toUnits x)⁻¹ = ↑x⁻¹
-- Mathlib.Topology.Defs.Filter
/-- Notation for the filter of right neighborhoods of a point.  -/
Topology.nhdsGE : Lean.ParserDescr
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {km : α},
  t.min? = some km → t.get! km = km
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSub.mk : ∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Sub G],
  autoParam (∀ (c : G), Measurable fun x => c - x) MeasurableSub.measurable_const_sub._autoParam →
    autoParam (∀ (c : G), Measurable fun x => x - c) MeasurableSub.measurable_sub_const._autoParam → MeasurableSub G
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
StieltjesFunction.mk.congr_simp : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (toFun toFun_1 : R → ℝ)
  (e_toFun : toFun = toFun_1) (mono' : Monotone toFun)
  (right_continuous' : ∀ (x : R), ContinuousWithinAt toFun (Set.Ici x) x),
  { toFun := toFun, mono' := mono', right_continuous' := right_continuous' } =
    { toFun := toFun_1, mono' := ⋯, right_continuous' := ⋯ }
-- Mathlib.Order.Partition.Basic
/-- For any set `t` containing no two distinct related elements, there is a representative function
equal to the identity on `t`.  -/
Partition.IsRepFun.exists_extend_partial' : ∀ {α : Type u_1} {t u : Set α} (P : Partition u),
  (∀ ⦃x y : α⦄, x ∈ t → y ∈ t → P.Rel x y → x = y) → ∃ f, P.IsRepFun f ∧ Set.EqOn f id t
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_neg : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f : M ⟶ N), ModuleCat.Hom.hom (-f) = -ModuleCat.Hom.hom f
-- Mathlib.Topology.UniformSpace.Defs
/-- A map `f : α → β` between uniform spaces is a *uniform embedding* if it is uniform inducing and
injective. If `α` is a separated space, then the latter assumption follows from the former.  -/
IsUniformEmbedding : {α : Type ua} → {β : Type ub} → [UniformSpace α] → [UniformSpace β] → (α → β) → Prop
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toListRev_ensureTermination_eq_match_step : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toListRev =
    match ↑it.step with
    | Std.IterStep.yield it' out => it'.toListRev ++ [out]
    | Std.IterStep.skip it' => it'.toListRev
    | Std.IterStep.done => []
-- Mathlib.Topology.Algebra.Order.UpperLower
IsLowerSet.closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α] {s : Set α},
  IsLowerSet s → IsLowerSet (closure s)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_isHomogeneous : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (f : M₁ →ₗ[R] M₂) (i : ι₂), (LinearMap.toMvPolynomial b₁ b₂ f i).IsHomogeneous 1
-- Mathlib.Data.Matrix.Mul
Matrix.nonUnitalNonAssocRing : {n : Type u_3} → {α : Type v} → [NonUnitalNonAssocRing α] → [Fintype n] → NonUnitalNonAssocRing (Matrix n n α)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  {p q : CategoryTheory.OverPresheafAux.YonedaCollection F X} (h : p.fst = q.fst),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) q.snd = p.snd → p = q
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.erase k Std.DTreeMap.Internal.Impl.leaf hr_1 =
    { impl := Std.DTreeMap.Internal.Impl.leaf, balanced_impl := ⋯, lb_le_size_impl := ⋯, size_impl_le_ub := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The projective point class underlying a nonsingular projective point on `W`.  -/
WeierstrassCurve.Projective.Point.point : {R : Type r} →
  [inst : CommRing R] → {W' : WeierstrassCurve.Projective R} → W'.Point → WeierstrassCurve.Projective.PointClass R
-- Mathlib.CategoryTheory.WithTerminal.FinCategory
/-- The equivalence between `Option C` and `WithInitial C` (they are both the
type `C` plus an extra object `none` or `star`).  -/
CategoryTheory.WithInitial.optionEquiv : (C : Type u) → Option C ≃ CategoryTheory.WithInitial C
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLE_map_toDual`. -/
List.SortedGE.of_map_toDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List α}, l.SortedGE → (List.map (⇑OrderDual.toDual) l).SortedLE
-- Lean.Meta.Tactic.Grind.PropagateInj
/-- If `e` is an application of the form `f a` where `f` is an injective function
in `(← get).inj.fns`, asserts `f⁻¹ (f a) = a`
 -/
Lean.Meta.Grind.mkInjEq : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_mk₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} {a : M} (f : CategoryTheory.ShiftedHom X Y a) (m₀ : M)
  (hm₀ : m₀ = 0) (g : Y ⟶ Z),
  f.comp (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ g) ⋯ =
    CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C a).map g)
-- Mathlib.Data.Set.Insert
Set.mem_insert_of_mem : ∀ {α : Type u_1} {x : α} {s : Set α} (y : α), x ∈ s → x ∈ insert y s
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.exists₂ : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₂ : ι₂},
  e₂.BoundaryGE i₂ → ∃ i₁, ac.Boundary i₁ i₂
-- Mathlib.Data.Setoid.Basic
/-- Given types `α`, `β`, the product of two equivalence relations `r` on `α` and `s` on `β`:
`(x₁, x₂), (y₁, y₂) ∈ α × β` are related by `r.prod s` iff `x₁` is related to `y₁`
by `r` and `x₂` is related to `y₂` by `s`.  -/
Setoid.prod : {α : Type u_1} → {β : Type u_2} → Setoid α → Setoid β → Setoid (α × β)
-- Mathlib.Data.Nat.DvdSequence
/-- **Alias** of `IsDvdSequence.smul`. -/
IsDivSequence.smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Dvd α] [inst_1 : Monoid β] [inst_2 : Monoid γ] {f : α → γ}
  [inst_3 : SMul β γ] [IsScalarTower β γ γ] [IsScalarTower β β γ] [SMulCommClass β γ γ] (b : β),
  IsDvdSequence f → IsDvdSequence (b • f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.forall_mem_keysArray_iff_forall_contains_getKey : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {p : α → Prop}, (∀ k ∈ (↑m).keysArray, p k) ↔ ∀ (k : α) (h : m.contains k = true), p (m.getKey k h)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toCycle_next : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {x : α} (f : Equiv.Perm α) (hf : f.IsCycle)
  (hx : x ∈ f.toCycle hf), (f.toCycle hf).next ⋯ x hx = f x
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.equivalence_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Idempotents.DoldKan.equivalence.inverse = CategoryTheory.Idempotents.DoldKan.Γ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_nonneg : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : NumberField.mixedEmbedding.mixedSpace K),
  0 ≤ (NumberField.mixedEmbedding.normAtPlace w) x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_filterMap_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)},
  (Std.DTreeMap.filterMap f t).size = t.size ↔ ∀ (a : α) (h : a ∈ t), (f a (t.get a h)).isSome = true
-- Mathlib.LinearAlgebra.BilinearMap
IsBilinearMap.add_left : ∀ {R : Type u_1} [inst : CommSemiring R] {E : Type u_2} [inst_1 : AddCommMonoid E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommMonoid F] [inst_4 : Module R F] {G : Type u_4} [inst_5 : AddCommMonoid G] [inst_6 : Module R G]
  {f : E → F → G}, IsBilinearMap R f → ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂) y = f x₁ y + f x₂ y
-- Lean.Level
/-- Reduce (if possible) universe level by 1  -/
Lean.Level.dec : Lean.Level → Option Lean.Level
-- Mathlib.LinearAlgebra.Pi
LinearMap.pi_proj : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)], LinearMap.pi LinearMap.proj = LinearMap.id
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_1.go : {motive_1 : Lean.Language.SnapshotTree → Sort u} →
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
    {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
      {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u} →
        {motive_5 : Task Lean.Language.SnapshotTree → Sort u} →
          (t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
            ((t : Lean.Language.SnapshotTree) → t.below → motive_1 t) →
              ((t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                  Lean.Language.SnapshotTree.below_1 t → motive_2 t) →
                ((t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                    Lean.Language.SnapshotTree.below_2 t → motive_3 t) →
                  ((t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) →
                      Lean.Language.SnapshotTree.below_3 t → motive_4 t) →
                    ((t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t) →
                      motive_2 t ×' Lean.Language.SnapshotTree.below_1 t
-- Mathlib.Analysis.Convex.StrictConvexBetween
/-- Given three collinear points, two (not equal) with distance `r` from `p` and one with
distance at most `r` from `p`, the third point is weakly between the other two points.  -/
Collinear.wbtw_of_dist_eq_of_dist_le : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] {p p₁ p₂ p₃ : P} {r : ℝ},
  Collinear ℝ {p₁, p₂, p₃} → dist p₁ p = r → dist p₂ p ≤ r → dist p₃ p = r → p₁ ≠ p₃ → Wbtw ℝ p₁ p₂ p₃
-- Mathlib.Topology.Compactness.Lindelof
/-- If `X` has a basis consisting of compact opens, then an open set in `X` is compact open iff
it is a finite union of some elements in the basis  -/
isLindelof_open_iff_eq_countable_iUnion_of_isTopologicalBasis : ∀ {X : Type u} {ι : Type u_1} [inst : TopologicalSpace X] (b : ι → Set X),
  TopologicalSpace.IsTopologicalBasis (Set.range b) →
    (∀ (i : ι), IsLindelof (b i)) → ∀ (U : Set X), IsLindelof U ∧ IsOpen U ↔ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i
-- Init.Data.Order.PackageFactories
Std.LinearPreorderPackage.toIsLinearPreorder : ∀ {α : Type u} [self : Std.LinearPreorderPackage α], Std.IsLinearPreorder α
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜), HasDerivAt id 1 x
-- Init.Data.List.Lemmas
List.headD_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {a : α}, (List.map f l).headD (f a) = f (l.headD a)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs
/-- This function measures the defect in `G2` being a modular form.  -/
EisensteinSeries.D2 : Matrix.SpecialLinearGroup (Fin 2) ℤ → UpperHalfPlane → ℂ
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLE.match_1.eq_3 : ∀ {α : Type u_1} (motive : WithBot α → WithBot α → Sort u_2) (a b : α) (h_1 : (x : WithBot α) → motive none x)
  (h_2 : (a : α) → motive (some a) none) (h_3 : (a b : α) → motive (some a) (some b)),
  (match some a, some b with
    | none, x => h_1 x
    | some a, none => h_2 a
    | some a, some b => h_3 a b) =
    h_3 a b
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.card_stabilizer_eq_card_inertia_mul_finrank : ∀ {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] (p : Ideal R)
  [inst_7 : p.IsPrime] (P : Ideal S) [P.LiesOver p] [P.IsPrime] [PerfectField p.ResidueField],
  Nat.card ↥(MulAction.stabilizer G P) = Nat.card ↥(Ideal.inertia G P) * P.inertiaDeg R
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.const_smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstSMul M X],
  AEMeasurable g μ → ∀ (c : M), AEMeasurable (c • g) μ
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.Gamma_eq_integral : ∀ {s : ℂ}, 0 < s.re → Complex.Gamma s = s.GammaIntegral
-- Init.Data.List.Basic
/-- Erases repeated elements, keeping the first element of each run.

`O(|l|)`.

Example:
* `[1, 3, 2, 2, 2, 3, 3, 5].eraseReps = [1, 3, 2, 3, 5]`
 -/
List.eraseReps : {α : Type u_1} → [BEq α] → List α → List α
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.adj_homEquiv : ∀ (V : Type u) [inst : CategoryTheory.ReflQuiver V] (C : Type u) [inst_1 : CategoryTheory.Category.{max u v, u} C],
  CategoryTheory.ReflQuiv.adj.homEquiv (CategoryTheory.ReflQuiv.of V) (CategoryTheory.Cat.of C) =
    (CategoryTheory.Cat.Hom.equivFunctor (CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of V))
          (CategoryTheory.Cat.of C)).trans
      CategoryTheory.ReflQuiv.adj.homEquiv
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
nndist_pi_lt_iff : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  {f g : (b : β) → X b} {r : NNReal}, 0 < r → (nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r)
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectSuccessorOf.single : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it' it : Std.IterM m β},
  it'.IsPlausibleSuccessorOf it → it'.IsPlausibleIndirectSuccessorOf it
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.posPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {μ : MeasureTheory.Measure α}
  [self : s.HaveLebesgueDecomposition μ], s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
-- Mathlib.RingTheory.Spectrum.Prime.TensorProduct
PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T],
  (algebraMap R T).SurjectiveOnStalks → Topology.IsEmbedding (PrimeSpectrum.tensorProductTo R S T)
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.cons.injEq : ∀ (a b a_1 b_1 : Mathlib.Deriving.Encodable.S✝),
  (Mathlib.Deriving.Encodable.S.cons✝ a b = Mathlib.Deriving.Encodable.S.cons✝ a_1 b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- `eqHom f f'`, for morphisms `f f' : j ⟶ j'`, is an arbitrary choice of morphism
`eqHom f f' : eq f f' ⟶ j` such that
`eq_condition : eqHom f f' ≫ f = eqHom f f' ≫ f'`.
Its existence is ensured by `IsCofiltered`.
 -/
CategoryTheory.IsCofiltered.eqHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {j j' : C} → (f f' : j ⟶ j') → CategoryTheory.IsCofiltered.eq f f' ⟶ j
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.coe_overEquivalence_functor_obj : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) (V : CategoryTheory.Over U),
  ↑(U.overEquivalence.functor.obj V) = Subtype.val ⁻¹' ↑V.left
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_σ_of_epi : ∀ {n : ℕ} (θ : { len := n + 1 } ⟶ { len := n }) [CategoryTheory.Epi θ], ∃ i, θ = SimplexCategory.σ i
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_map_eq_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f →
    ∀ (S : L.Substructure M), FirstOrder.Language.Substructure.comap f (FirstOrder.Language.Substructure.map f S) = S
-- Mathlib.Control.Bifunctor
Bifunctor.mk : {F : Type u₀ → Type u₁ → Type u₂} →
  ({α α' : Type u₀} → {β β' : Type u₁} → (α → α') → (β → β') → F α β → F α' β') → Bifunctor F
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
  (f =O[l] fun x => |u x|) ↔ f =O[l] u
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.comp_convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α},
  StrictConvexOn 𝕜 (f '' s) g → ConvexOn 𝕜 s f → MonotoneOn g (f '' s) → Set.InjOn f s → StrictConvexOn 𝕜 s (g ∘ f)
-- Mathlib.Tactic.Translate.GuessName
_private.Mathlib.Tactic.Translate.GuessName.0.Mathlib.Tactic.GuessName.fixAbbreviationAux.match_1.splitter : (motive : Option String → Sort u_1) →
  (x : Option String) → ((post : String) → motive (some post)) → (Unit → motive none) → motive x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.sameKeys_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Internal.Impl.map f t).SameKeys t
-- Mathlib.LinearAlgebra.Dual.Lemmas
Prod.instModuleIsReflexive : ∀ (R : Type u_1) (M : Type u_2) (N : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Module.IsReflexive R M]
  [Module.IsReflexive R N], Module.IsReflexive R (M × N)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientQuotientEquivQuotientₐ_mk_mk : ∀ {M : Type u_1} (R : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c d : RingCon M}
  (h : c ≤ d) (x : M), (RingCon.quotientQuotientEquivQuotientₐ R h) ⟦⟦x⟧⟧ = ⟦x⟧
-- Mathlib.Data.Set.Image
Set.disjoint_image_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α},
  Function.Injective f → (Disjoint (f '' s) (f '' t) ↔ Disjoint s t)
-- Mathlib.GroupTheory.GroupAction.Basic
Finite.of_finite_mulAction_orbitRel_quotient : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α] [Finite G]
  [Finite (MulAction.orbitRel.Quotient G α)], Finite α
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductDisjoint.of_cofan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} {c : CategoryTheory.Limits.Cofan X}
  (hc : CategoryTheory.Limits.IsColimit c) [∀ (i : ι), CategoryTheory.Mono (c.inj i)]
  (s : {i j : ι} → i ≠ j → CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j))
  (hs : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsLimit (s hij))
  (H : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsInitial (s hij).pt),
  CategoryTheory.Limits.CoproductDisjoint X