mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_keys : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keys.isEmpty = m.isEmpty
-- Std.Http.Data.Status
Std.Http.Status.other.inj : ∀ {status status_1 : Std.Http.CustomStatus},
  Std.Http.Status.other status = Std.Http.Status.other status_1 → status = status_1
-- Mathlib.CategoryTheory.Sites.EpiMono
CategoryTheory.Sheaf.instIsLocallySurjectiveAppArrowILocallySurjectiveLocallyInjectiveFunctorialLocallySurjectiveInjectiveFactorization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [inst_4 : J.WEqualsLocallyBijective A]
  (data : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData A)
  [inst_5 : CategoryTheory.HasWeakSheafify J A] (f : CategoryTheory.Arrow (CategoryTheory.Sheaf J A)),
  CategoryTheory.Sheaf.IsLocallySurjective
    ((CategoryTheory.Sheaf.functorialLocallySurjectiveInjectiveFactorization J data).i.app f)
-- Mathlib.Algebra.Order.SuccPred
PredSubOrder.pred_eq_sub_one : ∀ {α : Type u_1} {inst : Preorder α} {inst_1 : Sub α} {inst_2 : One α} [self : PredSubOrder α] (x : α),
  PredOrder.pred x = x - 1
-- Mathlib.RingTheory.Valuation.ValuationRing
Valuation.Integers.isFractionRing : ∀ {𝒪 : Type u} {K : Type v} {Γ : Type w} [inst : CommRing 𝒪] [inst_1 : Field K] [inst_2 : Algebra 𝒪 K]
  [inst_3 : LinearOrderedCommGroupWithZero Γ] {v : Valuation K Γ}, v.Integers 𝒪 → IsFractionRing 𝒪 K
-- Lean.Expr
Lean.Nat.mkType : Lean.Expr
-- Mathlib.SetTheory.ZFC.PSet
/-- Convert a pre-set to a `Set` of pre-sets.  -/
PSet.toSet : PSet.{u} → Set PSet.{u}
-- Mathlib.Tactic.Linter.Header
/-- Check the syntax `imports` for syntactically duplicate imports.
Two imports are considered duplicates only if they import the same module with the same modifiers.
For example, `public import Foo` and `import all Foo` are NOT duplicates.
 -/
_private.Mathlib.Tactic.Linter.Header.0.Mathlib.Linter.Style.header.duplicateImportsCheck : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_eq_of_sum_1 : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (t : Finset ι) {w : ι → R} (z : ι → E), ∑ i ∈ t, w i = 1 → t.centerMass w z = ∑ i ∈ t, w i • z i
-- Mathlib.Algebra.Star.Module
symm_starLinearEquiv : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : AddCommMonoid A]
  [inst_3 : StarAddMonoid A] [inst_4 : Module R A] [inst_5 : StarModule R A],
  (starLinearEquiv R).symm = starLinearEquiv R
-- Init.Data.Vector.Basic
Vector.instLE : {α : Type u_1} → {n : ℕ} → [LT α] → LE (Vector α n)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` reflects colimits of shape `Jᵒᵖ`, then `F.leftOp : Cᵒᵖ ⥤ D` reflects limits
of shape `J`.  -/
CategoryTheory.Limits.reflectsLimitsOfShape_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ)
  [CategoryTheory.Limits.ReflectsColimitsOfShape Jᵒᵖ F], CategoryTheory.Limits.ReflectsLimitsOfShape J F.leftOp
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.zeroLocus_empty_eq_univ : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}, X.zeroLocus ∅ = Set.univ
-- Init.Data.List.Perm
List.isEmpty.eq_2 : ∀ {α : Type u} (a : α) (as : List α), (a :: as).isEmpty = false
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.compress.eq_1 : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  (u v a : α), UV.compress u v a = if Disjoint u a ∧ v ≤ a then (a ⊔ u) \ v else a
-- Mathlib.Logic.Equiv.Defs
Equiv.arrowCongr_comp : ∀ {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ ≃ α₂)
  (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁),
  (ea.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.mk : {α : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid G] →
      {C : Set (Set α)} →
        (toFun : Set α → G) →
          toFun ∅ = 0 →
            (∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → toFun (⋃₀ ↑I) = ∑ u ∈ I, toFun u) →
              MeasureTheory.AddContent G C
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : t.modify k f ≠ ∅},
  (t.modify k f).maxKey he = if cmp (t.maxKey ⋯) k = Ordering.eq then k else t.maxKey ⋯
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- The function `update f a : X a → Π a, X a` is always measurable.
This doesn't require `f` to be measurable.
This should not be confused with the statement that `update f a x` is measurable.  -/
MeasureTheory.measurable_update_cylinderEvents : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ : Set ι} (f : (a : ι) → X a) {a : ι}
  [inst : DecidableEq ι], Measurable (Function.update f a)
-- Mathlib.Order.PFilter
Order.PFilter.dual : {P : Type u_1} → [inst : Preorder P] → Order.PFilter P → Order.Ideal Pᵒᵈ
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_map : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {it : Std.IterM m β} [inst_1 : Monad m]
  [LawfulMonad m] {f : β → β'},
  (Std.IterM.map f it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        let out' := f out;
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.map f it') out' ⋯))
      | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.map f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyOutgoingCallsParams : Lean.FromJson Lean.Lsp.CallHierarchyOutgoingCallsParams
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_add_left : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LT α] [i : AddRightStrictMono α] {b c : α}, b < c → ∀ (a : α), b + a < c + a
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.exists_right_inv : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a → ∃ b, a * b = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_add_heq : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n m : ℕ),
  p.take (n + m) ≍ (p.take n).append ((p.drop n).take m)
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instSDiffOfEquivBEqOfLawfulHashable : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → SDiff (Std.ExtHashSet α)
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_dropLast_getLast : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α}, List.Pairwise R l → ∀ (ha : a ∈ l.dropLast), R a (l.getLast ⋯)
-- Mathlib.Topology.Category.CompactlyGenerated
/-- Constructor for objects of the category `CompactlyGenerated`.  -/
CompactlyGenerated.of : (X : Type w) → [inst : TopologicalSpace X] → [UCompactlyGeneratedSpace X] → CompactlyGenerated
-- Mathlib.Algebra.Algebra.Tower
/-- See note [partially-applied ext lemmas].  -/
IsScalarTower.of_algebraMap_eq' : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A],
  algebraMap R A = (algebraMap S A).comp (algebraMap R S) → IsScalarTower R S A
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.instGroupAutGalois : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) → Group (CategoryTheory.PreGaloisCategory.AutGalois F)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.coe_one : ∀ {G : Type u_1} [inst : Add G] {a : G}, ⇑1 = id
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- Let `t i` be a nonempty countable family of measurable sets in `α`. Let `g i : α → β` be a
family of measurable functions such that `g i` agrees with `g j` on `t i ∩ t j`. Then there exists
a measurable function `f : α → β` that agrees with each `g i` on `t i`.

We only need the assumption `[Nonempty ι]` to prove `[Nonempty (α → β)]`.  -/
exists_measurable_piecewise : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {ι : Type u_6} [Countable ι]
  [Nonempty ι] (t : ι → Set α),
  (∀ (n : ι), MeasurableSet (t n)) →
    ∀ (g : ι → α → β),
      (∀ (n : ι), Measurable (g n)) →
        (Pairwise fun i j => Set.EqOn (g i) (g j) (t i ∩ t j)) → ∃ f, Measurable f ∧ ∀ (n : ι), Set.EqOn f (g n) (t n)
-- Init.PropLemmas
not_imp_of_and_not : ∀ {a b : Prop}, a ∧ ¬b → ¬(a → b)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The `i`th canonical injection, from `A i` to the free product  -/
LinearAlgebra.FreeProduct.ι : {I : Type u_1} →
  [inst : DecidableEq I] →
    (R : Type u_2) →
      [inst_1 : CommSemiring R] →
        (A : I → Type u_3) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] → (i : I) → A i →ₐ[R] LinearAlgebra.FreeProduct R A
-- Mathlib.Analysis.Complex.Basic
/-- The only continuous ring homomorphisms from `ℂ` to `ℂ` are the identity and the complex
conjugation.  -/
Complex.ringHom_eq_id_or_conj_of_continuous : ∀ {f : ℂ →+* ℂ}, Continuous ⇑f → f = RingHom.id ℂ ∨ f = starRingEnd ℂ
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- The fields of `StrictSegal` define an equivalence between `X _⦋n⦌`
and `Path X n`.  -/
SSet.StrictSegal.spineEquiv : {X : SSet} → X.StrictSegal → (n : ℕ) → X.obj (Opposite.op { len := n }) ≃ X.Path n
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendHom.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ s.pt),
  s.extendHom f = { hom := f, w := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsRightCancelAdd.addRightStrictMono_of_addRightMono : ∀ (N : Type u_2) [inst : Add N] [IsRightCancelAdd N] [inst_2 : PartialOrder N] [AddRightMono N], AddRightStrictMono N
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.Disjoint.card_support_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.Disjoint g → (f * g).support.card = f.support.card + g.support.card
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.rankInfinite_of_infinite : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → B.Infinite → M.RankInfinite
-- Mathlib.Algebra.Algebra.Tower
Submodule.smul_mem_span_smul : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [IsScalarTower R S A] {s : Set S},
  Submodule.span R s = ⊤ → ∀ {t : Set A} {k : S} {x : A}, x ∈ Submodule.span R t → k • x ∈ Submodule.span R (s • t)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.go.match_13.splitter : (motive : Std.Sat.AIG.Decl ℕ → Sort u_1) →
  (decl : Std.Sat.AIG.Decl ℕ) →
    (decl = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false) →
      ((idx : ℕ) → decl = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx)) →
        ((lhs rhs : Std.Sat.AIG.Fanin) →
            decl = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)) →
          motive decl
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.length_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.toList.length = t.size
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.instPartialOrder : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] → [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → PartialOrder (StarSubalgebra R A)
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal_filter_le_snd_of_le : ∀ {n k : ℕ},
  k ≤ n →
    {a ∈ Finset.HasAntidiagonal.antidiagonal n | k ≤ a.2} =
      Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ })
        (Finset.HasAntidiagonal.antidiagonal (n - k))
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go.eq_2 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (x : α) (i j : ℕ) (y : α)
  (ys : List α),
  List.minIdxOn.go✝ f x i j (y :: ys) =
    if f x ≤ f y then List.minIdxOn.go✝ f x i (j + 1) ys else List.minIdxOn.go✝ f y j (j + 1) ys
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` reflects colimits, then `F : Cᵒᵖ ⥤ D` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_of_rightOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [CategoryTheory.Limits.ReflectsColimits F.rightOp],
  CategoryTheory.Limits.ReflectsLimits F
-- Mathlib.Order.Filter.Pointwise
Filter.le_one_iff : ∀ {α : Type u_2} [inst : One α] {f : Filter α}, f ≤ 1 ↔ 1 ∈ f
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMap₂_toMatrix₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Fintype n] [inst_8 : Fintype m]
  [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁) (b₂ : Module.Basis m R M₂)
  (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂), (Matrix.toLinearMap₂ b₁ b₂) ((LinearMap.toMatrix₂ b₁ b₂) B) = B
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.id : {B : Type u} →
  [inst : Quiver B] → {a b : CategoryTheory.FreeBicategory B} → (f : a ⟶ b) → CategoryTheory.FreeBicategory.Hom₂ f f
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β}, List.Pairwise (fun a b => (a.1 == b.1) = false) l → (k, v) ∈ l → (m.insertMany l)[k']! = v
-- Mathlib.MeasureTheory.Measure.Restrict
Filter.EventuallyEq.restrict : ∀ {α : Type u_2} {δ : Type u_4} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → δ} {s : Set α},
  f =ᵐ[μ] g → f =ᵐ[μ.restrict s] g
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.exists_finset_of_mem_supr'' : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Type u_3}
  {f : ι → IntermediateField F E},
  (∀ (i : ι), Algebra.IsAlgebraic F ↥(f i)) →
    ∀ {x : E}, x ∈ ⨆ i, f i → ∃ s, x ∈ ⨆ i ∈ s, IntermediateField.adjoin F ((minpoly F i.snd).rootSet E)
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The universal property of the tensor product of algebras.

Pairs of algebra morphisms that commute are equivalent to algebra morphisms from the tensor product.

This is `Algebra.TensorProduct.lift` as an equivalence.

See also `GradedTensorProduct.liftEquiv` for an alternative commutativity requirement for graded
algebra.  -/
Algebra.TensorProduct.liftEquiv : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        {C : Type uC} →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : Algebra R S] →
                [inst_3 : Semiring A] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra S A] →
                      [inst_6 : IsScalarTower R S A] →
                        [inst_7 : Semiring B] →
                          [inst_8 : Algebra R B] →
                            [inst_9 : Semiring C] →
                              [inst_10 : Algebra S C] →
                                [inst_11 : Algebra R C] →
                                  [IsScalarTower R S C] →
                                    { fg // ∀ (x : A) (y : B), Commute (fg.1 x) (fg.2 y) } ≃
                                      (TensorProduct R A B →ₐ[S] C)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero : ∀ {R : Type u_2} [inst : Field R] (g : Matrix.SpecialLinearGroup (Fin 2) R),
  ↑g 1 0 = 0 → ∃ a b, ∃ (h : a ≠ 0), g = ⟨!![a, b; 0, a⁻¹], ⋯⟩
-- Mathlib.Data.List.OffDiag
List.Nodup.offDiag : ∀ {α : Type u_1} {l : List α}, l.Nodup → l.offDiag.Nodup
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.postcompCLM_postcompCLM : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} {G : Type u_7} {H : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedAddCommGroup G] [inst_7 : NormedSpace ℝ G] [inst_8 : NormedSpace 𝕜 G]
  [inst_9 : NormedAddCommGroup H] [inst_10 : NormedSpace ℝ H] [inst_11 : NormedSpace 𝕜 H] (L₁ : F →L[𝕜] G)
  (L₂ : G →L[𝕜] H) (f : SchwartzMap E F),
  (SchwartzMap.postcompCLM L₂) ((SchwartzMap.postcompCLM L₁) f) = (SchwartzMap.postcompCLM (L₂ ∘SL L₁)) f
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.setLIntegral_kernel_prod_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : α → β → ENNReal},
  Measurable (Function.uncurry f) → ∀ {s : Set β}, MeasurableSet s → Measurable fun a => ∫⁻ (b : β) in s, f a b ∂κ a
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
/-- The equivariant map from embeddings of `Fin n` (aka arrangement) to combinations.  -/
Set.powersetCard.mulActionHom_of_embedding : (G : Type u_1) →
  [inst : Group G] →
    (α : Type u_2) →
      [inst_1 : MulAction G α] → (n : ℕ) → [inst_2 : DecidableEq α] → (Fin n ↪ α) →ₑ[id] ↑(Set.powersetCard α n)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.instElemOrbit_1.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (x : MulAction.orbitRel.Quotient G α),
  MulAction.instElemOrbit_1 x =
    { smul := fun g => Set.MapsTo.restrict (fun x => g • x) x.orbit x.orbit ⋯, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
  Measurable f →
    ∀ (g : α → ENNReal) {s : Set α},
      MeasurableSet s →
        (∀ᵐ (x : α) ∂μ.restrict s, f x < ⊤) → ∫⁻ (a : α) in s, g a ∂μ.withDensity f = ∫⁻ (a : α) in s, (f * g) a ∂μ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_eq_fallback : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a fallback : α}, a ∉ m → m.getD a fallback = fallback
-- Mathlib.Data.Num.Lemmas
Num.commSemiring : CommSemiring Num
-- Mathlib.Algebra.GroupWithZero.Basic
/-- Dividing `a` by itself and then multiplying by itself results in `a`, whether or not `a` is
zero.  -/
div_self_mul_self : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a / a * a = a
-- Mathlib.Order.Basic
Subtype.mk_le_mk : ∀ {α : Type u_2} [inst : LE α] {p : α → Prop} {x y : α} {hx : p x} {hy : p y}, ⟨x, hx⟩ ≤ ⟨y, hy⟩ ↔ x ≤ y
-- Init.Data.Int.Gcd
Int.lcm_dvd_natAbs_mul : ∀ (m n : ℤ), m.lcm n ∣ m.natAbs * n.natAbs
-- Std.Sat.AIG.If
Std.Sat.AIG.mkIfCached : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.TernaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.Algebra.Group.Opposite
MulOpposite.semiconjBy_op : ∀ {α : Type u_1} [inst : Mul α] {a x y : α},
  SemiconjBy (MulOpposite.op a) (MulOpposite.op y) (MulOpposite.op x) ↔ SemiconjBy a x y
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ofArray_fold_fn.match_1.eq_3 : ∀ {n : ℕ} (motive : Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) → Sort u_1)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (h_1 : Unit → motive none)
  (h_2 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, true)))
  (h_3 : (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → motive (some (l, false))),
  (match some (l, false) with
    | none => h_1 ()
    | some (l, true) => h_2 l
    | some (l, false) => h_3 l) =
    h_3 l
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity : Type
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
interior, and `f''` is nonnegative on the interior, then `f` is convex on `D`.  -/
convexOn_of_hasDerivWithinAt2_nonneg : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f f' f'' : ℝ → ℝ},
      ContinuousOn f D →
        (∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) →
          (∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x) →
            (∀ x ∈ interior D, 0 ≤ f'' x) → ConvexOn ℝ D f
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.flatMapM.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (a : α) (as : List α) (bs : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs),
  (match a :: as, bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_2 a as bs
-- Lean.Meta.Tactic.Induction
Lean.Meta.instInhabitedAltVarNames.default : Lean.Meta.AltVarNames
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.listR.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode.Path α),
  x.listR =
    match x with
    | RBTree.RBNode.Path.root => []
    | RBTree.RBNode.Path.left c parent v r => v :: r.toList ++ parent.listR
    | RBTree.RBNode.Path.right c l v parent => parent.listR
-- Mathlib.RepresentationTheory.Basic
Representation.ofMulAction_single : ∀ {k : Type u_1} [inst : Semiring k] {G : Type u_2} [inst_1 : Monoid G] {H : Type u_3} [inst_2 : MulAction G H] (g : G)
  (x : H) (r : k), ((Representation.ofMulAction k G H) g) (MonoidAlgebra.single x r) = MonoidAlgebra.single (g • x) r
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) {n : ℕ},
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op { len := n })).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
      (AlgebraicTopology.DoldKan.PInfty.f n) =
    ((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op { len := n })).inj
      (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.binomial_nonneg : ∀ {n : ℕ} {p : ↑unitInterval} {k : ℕ}, 0 ≤ ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)
-- Aesop.Tracing
Aesop.traceSimpTheorems : Lean.Meta.SimpTheorems → Aesop.TraceOption → Lean.CoreM Unit